diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-06-28 07:59:03 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-06-28 07:59:03 +0000 |
commit | 5312915c1b29929f82e1f8de80609a277584913f (patch) | |
tree | 0f7ee475743f0eb05d352148a9e1f0b861ee9d34 /pg | |
parent | f3250c32ff42ae18fd03a5311c1f0caec3415aba (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-x | pg | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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\")" \ |