diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-08-28 22:39:41 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-08-28 22:39:41 +0200 |
| commit | 23a129e18ae930de5f40df59307c48c68d62d8d7 (patch) | |
| tree | 403387a98ea9da32d70ac5b5607d5be30fa0ee42 /pg | |
| parent | 780ad9d001af651a49d7470e963ed9a49ee11a4c (diff) | |
| parent | 192bd462233d0284fa3d5f8e8994a514b549713e (diff) | |
| download | compcert-kvx-23a129e18ae930de5f40df59307c48c68d62d8d7.tar.gz compcert-kvx-23a129e18ae930de5f40df59307c48c68d62d8d7.zip | |
Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge
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 |