aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-05-18 07:31:36 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-01 15:50:26 +0200
commit6b041a242607ec906fbab451e53c15af6339e4ef (patch)
treeac7b4e6a25c0607c1770da551ed4f5de4addb310 /test-suite/output
parentf3a388baf9cf2a14a658cab77554a0802b999486 (diff)
[emacs] [toplevel] Make emacs flag local to the toplevel.
We remove the emacs-specific printing code from the core of Coq, now `-emacs` is a printing flag controlled by the toplevel.
Diffstat (limited to 'test-suite/output')
-rw-r--r--test-suite/output/Show.out2
1 files changed, 0 insertions, 2 deletions
diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out
index 8acfed5d0..ca56f032f 100644
--- a/test-suite/output/Show.out
+++ b/test-suite/output/Show.out
@@ -8,5 +8,3 @@ subgoal 2 (ID 35) is:
1 = S (S m')
subgoal 3 (ID 22) is:
S (S n') = S m
-
-(dependent evars: (printing disabled) )