index
:
compcert
FPcomp
aarch64
conditional-move
dev/michalis
floatofintu
inl-cse-const
master
no-pervasives
CompCert fork with minor modifications for Vericert.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
coq
diff options
context:
1
2
3
4
5
6
7
8
9
10
15
20
25
30
35
40
space:
include
ignore
mode:
unified
ssdiff
stat only
Diffstat
(limited to 'coq')
-rwxr-xr-x
coq
2
1 files changed, 1 insertions, 1 deletions
diff --git a/coq b/coq
index ea088059..0b04a8c7 100755
--- a/
coq
+++ b/
coq
@@ -12,4 +12,4 @@ make -q ${1}o || {
done)
}
-coqide $INCLUDES $1 && make ${1}o
+"${COQBIN}coqide" $INCLUDES $1 && make ${1}o