From ff1ead9fe0d816918f13e1586ecfed321f4a3bf3 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Sat, 3 Aug 2019 09:11:42 +0200
Subject: Simplify invocation of Emacs + Proof General

PG now uses the _Coqproject file and finds relevant paths there.
---
 pg | 20 +++-----------------
 1 file changed, 3 insertions(+), 17 deletions(-)

(limited to 'pg')

diff --git a/pg b/pg
index 28926baa..398d618f 100755
--- a/pg
+++ b/pg
@@ -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
-- 
cgit