From 77f1db2c35d3d337f4a47dc98d02f3c4749d9ade Mon Sep 17 00:00:00 2001
From: courtieu
Date: Tue, 24 May 2011 19:01:42 +0000
Subject: Made the emacs-U option deprecated. Also removed the old code
 inserting special chars for proof by pointing with emacs. This was
 interacting badly with utf8. It may be implemented back with xml-like tags
 instead of special chars.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14154 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/flags.ml  | 1 -
 lib/flags.mli | 1 -
 2 files changed, 2 deletions(-)

(limited to 'lib')

diff --git a/lib/flags.ml b/lib/flags.ml
index 547e394aa3..e8763bc79f 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -23,7 +23,6 @@ let batch_mode = ref false
 let debug = ref false
 
 let print_emacs = ref false
-let print_emacs_safechar = ref false
 
 let term_quality = ref false
 
diff --git a/lib/flags.mli b/lib/flags.mli
index dd0f33ae4c..f7e3c17597 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -15,7 +15,6 @@ val batch_mode : bool ref
 val debug : bool ref
 
 val print_emacs : bool ref
-val print_emacs_safechar : bool ref
 
 val term_quality : bool ref
 
-- 
cgit v1.2.3