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 - 1 file changed, 1 deletion(-) (limited to 'lib/flags.ml') diff --git a/lib/flags.ml b/lib/flags.ml index 547e394aa..e8763bc79 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 -- cgit v1.2.3