From 1681238424c2d46e7a31467212d4daed4b30a827 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 13 Jun 2014 17:04:05 +0200
Subject: Deprecate useless option -quality.

---
 lib/flags.ml  | 2 --
 lib/flags.mli | 2 --
 2 files changed, 4 deletions(-)

(limited to 'lib')

diff --git a/lib/flags.ml b/lib/flags.ml
index 5fba48dd62..7fed951008 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -64,8 +64,6 @@ let profile = false
 
 let print_emacs = ref false
 
-let term_quality = ref false
-
 let xml_export = ref false
 
 let ide_slave = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index b5947c48f0..c1e5a9dbd0 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -28,8 +28,6 @@ val profile : bool
 
 val print_emacs : bool ref
 
-val term_quality : bool ref
-
 val xml_export : bool ref
 
 val ide_slave : bool ref
-- 
cgit v1.2.3