aboutsummaryrefslogtreecommitdiffhomepage
path: root/scripts
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-04-12 20:49:01 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-04-12 20:49:01 +0000
commit59c9403ceb09a35ed219b522e9f5abdb50615d76 (patch)
treef7d3e521f6a948defdce70e00c718c6bdc7b696e /scripts
parent1b9428c4e4ce6f2dbe98d0f753b062ae8634a954 (diff)
lib directory is cut in 2 cma.
- Clib that does not depend on camlpX and is made to be shared by all coq tools/scripts/... - Lib that is Coqtop specific As a side effect for the build system : - Coq_config is in Clib and does not appears in makefiles - only the BEST version of coqc and coqmktop is made - ocamlbuild build system fails latter but is still broken (ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
-rw-r--r--scripts/coqc.ml3
-rw-r--r--scripts/coqmktop.ml2
2 files changed, 2 insertions, 3 deletions
diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index ce92b9118..e62a9d2f8 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -150,8 +150,7 @@ let parse_args () =
parse (cfiles,o::args) rem
| ("-where") :: _ ->
- (try print_endline (Envars.coqlib ())
- with Errors.UserError(_,pps) -> Pp.msgerrnl (Pp.hov 0 pps));
+ print_endline (Envars.coqlib (fun x -> x));
exit 0
| ("-config" | "--config") :: _ -> Usage.print_config (); exit 0
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index d0132763a..55e12a30e 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -56,7 +56,7 @@ let src_dirs () =
[ []; ["kernel";"byterun"]; [ "config" ]; [ "toplevel" ] ]
let includes () =
- let coqlib = Envars.coqlib () in
+ let coqlib = Envars.coqlib Errors.error in
let camlp4lib = Envars.camlp4lib () in
List.fold_right
(fun d l -> "-I" :: ("\"" ^ List.fold_left Filename.concat coqlib d ^ "\"") :: l)