aboutsummaryrefslogtreecommitdiffstats
path: root/coq
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2020-09-21 14:15:31 +0200
committerXavier Leroy <xavier.leroy@college-de-france.fr>2020-09-21 14:15:31 +0200
commitb525fbe0915931a939d5851b511ce46fcf026236 (patch)
tree8117697dbb9289a3b662e98522b9fc4065b7aaab /coq
parente7b938f620ddc1e10542727f7ec142f47f7090bf (diff)
downloadcompcert-kvx-b525fbe0915931a939d5851b511ce46fcf026236.tar.gz
compcert-kvx-b525fbe0915931a939d5851b511ce46fcf026236.zip
No need for -R options, _CoqProject contains them already
Diffstat (limited to 'coq')
-rwxr-xr-xcoq6
1 files changed, 2 insertions, 4 deletions
diff --git a/coq b/coq
index fcf744fd..925bc4b9 100755
--- a/coq
+++ b/coq
@@ -1,10 +1,8 @@
#!/bin/sh
-# Start coqide with the right -I options
+# Start coqide with the right options
# Use the Makefile to rebuild dependencies if needed
# Recompile the modified file after coqide editing
-INCLUDES=`make print-includes`
-
make -q ${1}o || {
make -n ${1}o | grep -v "\\b${1}\\b" | \
(while read cmd; do
@@ -12,4 +10,4 @@ make -q ${1}o || {
done)
}
-"${COQBIN}coqide" -async-proofs off $INCLUDES $1 && make ${1}o
+"${COQBIN}coqide" -async-proofs off $1 && make ${1}o