aboutsummaryrefslogtreecommitdiffhomepage
path: root/scripts
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-01-10 22:37:15 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-01-10 22:37:15 +0000
commitdb6363f65f8c68ccadd39effe76a5142c8ee1acd (patch)
tree4f7967725385a884fb51b17c1833e655e5180d30 /scripts
parentee2110587e91f288bcae62e9f837f99079dfaf2a (diff)
- Fixed the recompilation of config/revision.ml once every two conmpilations.
- Fixed an error message in configure - Support for filenames with spaces in coqmktop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11772 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
-rw-r--r--scripts/coqmktop.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index b765f8620..f41042807 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -59,7 +59,7 @@ let includes () =
let coqlib = Envars.coqlib () in
let camlp4lib = Envars.camlp4lib () in
List.fold_right
- (fun d l -> "-I" :: List.fold_left Filename.concat coqlib d :: l)
+ (fun d l -> "-I" :: ("\"" ^ List.fold_left Filename.concat coqlib d ^ "\"") :: l)
(src_dirs ())
(["-I"; "\"" ^ camlp4lib ^ "\""] @
["-I"; "\"" ^ coqlib ^ "\""] @