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
100
100
.PHONY : this-config this-build this-only this-test-suite this-test-suite-stdlib this-distclean this-clean
101
101
102
102
this-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 \
105
105
echo ' already configured' ; \
106
106
else\
107
107
coqc --print-version > config.stamp; \
@@ -113,7 +113,7 @@ this-config:: __always__
113
113
sed -i.bak -e ' s/From Corelib/From Coq/' ` find . -name \* .v` ; \
114
114
sed -i.bak -e ' s/IntDef/ZArith/' ` find . -name \* .v` ; \
115
115
fi ; \
116
- fi
116
+ fi ; fi
117
117
# Remove all of the above when requiring Rocq >= 9.0
118
118
119
119
this-build :: this-config Makefile.coq
You can’t perform that action at this time.
0 commit comments