diff options
| author | herbelin | 2008-03-09 12:36:54 +0000 |
|---|---|---|
| committer | herbelin | 2008-03-09 12:36:54 +0000 |
| commit | 83675746b37df4ec670124f045fb1f13c0c7db1f (patch) | |
| tree | 54b06ef23891982d0044f01c053077fc61a09fd3 /scripts | |
| parent | 311b326b3e3a317cfd309e17dafc8e77e6def49b (diff) | |
Des choses bizarres avec pa_op.cmo (extension syntaxique pour parser)
se passent avec camlp5 qui ne se passaient pas avec l'ancien camlp4:
pa_op.cmo exige camlp5o.cma mais alors, il y a un message de
redéfinition de ipatt que je ne sais pas éviter avec
coqtop.byte. Puisque pa_op.cmo n'est finalement pas utile, on le
retire.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10646 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
| -rw-r--r-- | scripts/coqmktop.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index aeeb2e1346..bd155abfe8 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -33,7 +33,7 @@ let ide = split_list Tolink.ide (* 3. Toplevel objects *) let camlp4topobjs = if Coq_config.camlp4 = "camlp5" then - ["camlp5_top.cma"; "camlp5o.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"] + ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"] else ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"] let topobjs = camlp4topobjs @@ -102,7 +102,7 @@ let files_to_link userfiles = ((List.map native_suffix objs) @ userfiles, (List.map native_suffix libs) @ userfiles) else - (objs @ userfiles ,libs @ userfiles ) + (objs @ userfiles, libs @ userfiles ) in let modules = List.map module_of_file objstolink in (modules, libstolink) @@ -297,7 +297,7 @@ let main () = (*file for dynlink *) let dynlink= if not (!opt || !top) then - [tmp_dynlink()] + [(print_int 2; tmp_dynlink())] else [] in @@ -318,6 +318,7 @@ let main () = (string_of_int (String.length command)) ^ " characters)"); flush Pervasives.stdout end; + print_string command; let retcode = Sys.command command in clean main_file; (* command gives the exit code in HSB, and signal in LSB !!! *) |