diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-08-03 09:11:42 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-08-05 16:33:59 +0200 |
commit | ff1ead9fe0d816918f13e1586ecfed321f4a3bf3 (patch) | |
tree | 8a009f064a48b1d09a4276c08ef53ffaf6fad42a /pg | |
parent | 91381b65f5aa76e5195caae9ef331b3f5f95afaf (diff) | |
download | compcert-ff1ead9fe0d816918f13e1586ecfed321f4a3bf3.tar.gz compcert-ff1ead9fe0d816918f13e1586ecfed321f4a3bf3.zip |
Simplify invocation of Emacs + Proof General
PG now uses the _Coqproject file and finds relevant paths there.
Diffstat (limited to 'pg')
-rwxr-xr-x | pg | 20 |
1 files changed, 3 insertions, 17 deletions
@@ -1,10 +1,7 @@ #!/bin/sh -# Start Proof General with the right -I options +# Start Proof General with the right Coq version # Use the Makefile to rebuild dependencies if needed -# Recompile the modified file after coqide editing - -PWD=`pwd` -INCLUDES=`make print-includes` +# Recompile the modified file after editing make -q ${1}o || { make -n ${1}o | grep -v "\\b${1}\\b" | \ @@ -15,16 +12,5 @@ make -q ${1}o || { COQPROGNAME="${COQBIN}coqtop" -COQPROGARGS="" -for arg in $INCLUDES; do - case "$arg" in - -I|-R|-as|compcert*) - COQPROGARGS="$COQPROGARGS \"$arg\"";; - *) - COQPROGARGS="$COQPROGARGS \"$PWD/$arg\"";; - esac -done - -emacs --eval "(setq coq-prog-name \"$COQPROGNAME\")" \ - --eval "(setq coq-prog-args '($COQPROGARGS))" $1 \ +emacs --eval "(setq coq-prog-name \"$COQPROGNAME\")" $1 \ && make ${1}o |