summaryrefslogtreecommitdiff
path: root/pg
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-06-28 07:59:03 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-06-28 07:59:03 +0000
commit5312915c1b29929f82e1f8de80609a277584913f (patch)
tree0f7ee475743f0eb05d352148a9e1f0b861ee9d34 /pg
parentf3250c32ff42ae18fd03a5311c1f0caec3415aba (diff)
Use Flocq for floats
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'pg')
-rwxr-xr-xpg2
1 files changed, 1 insertions, 1 deletions
diff --git a/pg b/pg
index d63be34..9242303 100755
--- a/pg
+++ b/pg
@@ -15,7 +15,7 @@ make -q ${1}o || {
done)
}
COQPROGNAME="coqtop"
-COQPROGARGS="\"-I\" \"$PWD/lib\" \"-I\" \"$PWD/common\" \"-I\" \"$VARIANT\" \"-I\" \"$ARCH\" \"-I\" \"$PWD/backend\" \"-I\" \"$PWD/cfrontend\""
+COQPROGARGS="\"-I\" \"$PWD/lib\" \"-I\" \"$PWD/common\" \"-I\" \"$VARIANT\" \"-I\" \"$ARCH\" \"-I\" \"$PWD/backend\" \"-I\" \"$PWD/cfrontend\" \"-I\" \"$PWD/flocq\" \"-I\" \"$PWD/flocq/Appli\" \"-I\" \"$PWD/flocq/Calc\" \"-I\" \"$PWD/flocq/Core\" \"-I\" \"$PWD/flocq/Prop\""
emacs --eval "(setq coq-prog-name \"$COQPROGNAME\")" \