diff options
author | courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-11-24 13:39:11 +0000 |
---|---|---|
committer | courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-11-24 13:39:11 +0000 |
commit | a2ff83f35f47f2aa3b63f224b988a086b19c00b4 (patch) | |
tree | 49205053682094cffd1f12648d840ce4802ecc16 | |
parent | 7299989ccd2ff0eca2dc934b08ba05290ac001bb (diff) |
Fixed the -emacs option which was always On.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9402 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | toplevel/toplevel.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index f75b8fc68..7f21de041 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -220,7 +220,8 @@ let make_emacs_prompt() = (fun acc x -> acc ^ (if acc <> "" then "|" else "") ^ Names.string_of_id x) "" pending in let proof_info = if dpth >= 0 then string_of_int dpth else "0" in - statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " ^ (emacs_prompt_endstring()) + if !Options.print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " + else "" (* A buffer to store the current command read on stdin. It is * initialized when a vernac command is immediately followed by "\n", @@ -230,6 +231,7 @@ let top_buffer = emacs_prompt_startstring() ^ make_prompt() ^ make_emacs_prompt() + ^ emacs_prompt_endstring() in { prompt = pr; str = ""; |