diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-12 14:55:24 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-12 14:55:24 +0000 |
| commit | c5301d16345e4d3c6b332cc73e7b66d7b915341a (patch) | |
| tree | b1deceb04ca8dc2aaaa2aa358ce77307ad4af37a /toplevel | |
| parent | 18ff5c1f279194fd55033744b733a32291d0bba9 (diff) | |
petit bug -byte/-opt (execv -> execvp) et message coercion teste is_silent
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1086 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 11 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 6 |
2 files changed, 12 insertions, 5 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 2d6a9f2af..5ece34630 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -63,11 +63,16 @@ let require () = let re_exec s = let is_native = (Mltop.get()) = Mltop.Native in - if (is_native && s = "byte") || ((not is_native) && s = "opt") then + if (is_native && s = "byte") || ((not is_native) && s = "opt") then begin let prog = Sys.argv.(0) in - let newprog = Filename.concat (Filename.dirname prog) ("coqtop." ^ s) in + let newprog = + let dir = Filename.dirname prog in + let com = "coqtop." ^ s in + if dir <> "." then Filename.concat dir com else com + in Sys.argv.(0) <- newprog; - Unix.execv newprog Sys.argv + Unix.execvp newprog Sys.argv + end (* Parsing of the command line. * diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 54fcda305..47675e0df 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -811,7 +811,8 @@ let _ = definition_body_red red_option id (local,stre) c typ_opt; if coe then begin Class.try_add_new_coercion id stre; - message ((string_of_id id) ^ " is now a coercion") + if (not (is_silent())) then + message ((string_of_id id) ^ " is now a coercion") end; if idcoe then Class.try_add_new_coercion_subclass id stre; @@ -1247,7 +1248,8 @@ let _ = let isid = identity = "IDENTITY" in fun () -> Class.try_add_new_coercion_with_target id stre ids idt isid; - message ((string_of_id id) ^ " is now a coercion") + if (not (is_silent())) then + message ((string_of_id id) ^ " is now a coercion") | _ -> bad_vernac_args "COERCION") let _ = |