File tree Expand file tree Collapse file tree 1 file changed +3
-3
lines changed Expand file tree Collapse file tree 1 file changed +3
-3
lines changed Original file line number Diff line number Diff line change @@ -100,8 +100,8 @@ distclean: sub-distclean this-distclean
100100.PHONY : this-config this-build this-only this-test-suite this-test-suite-stdlib this-distclean this-clean
101101
102102this-config :: __always__
103- @command -v coqc > /dev/null || exit 0 # Maybe on Rocq (without coq shim), nothing to do anyway
104- @ if [ -e config.stamp -a " ` coqc --print-version` " = " ` cat config.stamp 2> /dev/null` " ] ; then \
103+ @if $$( command -v coqc >/dev/null ) ; then \
104+ if [ -e config.stamp -a " ` coqc --print-version` " = " ` cat config.stamp 2> /dev/null` " ] ; then \
105105 echo ' already configured' ; \
106106 else\
107107 coqc --print-version > config.stamp; \
@@ -113,7 +113,7 @@ this-config:: __always__
113113 sed -i.bak -e ' s/From Corelib/From Coq/' ` find . -name \* .v` ; \
114114 sed -i.bak -e ' s/IntDef/ZArith/' ` find . -name \* .v` ; \
115115 fi ; \
116- fi
116+ fi ; fi
117117 # Remove all of the above when requiring Rocq >= 9.0
118118
119119this-build :: this-config Makefile.coq
You can’t perform that action at this time.
0 commit comments