aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-11-24 13:39:11 +0000
committerGravatar courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-11-24 13:39:11 +0000
commita2ff83f35f47f2aa3b63f224b988a086b19c00b4 (patch)
tree49205053682094cffd1f12648d840ce4802ecc16
parent7299989ccd2ff0eca2dc934b08ba05290ac001bb (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.ml4
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 = "";