From 2def58217686b5083da38778a5ebffb451b1d4d6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 12 Jun 2017 22:12:02 +0200 Subject: [flags] Remove XML output flag. This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied. --- lib/flags.mli | 5 ----- 1 file changed, 5 deletions(-) (limited to 'lib/flags.mli') diff --git a/lib/flags.mli b/lib/flags.mli index eb4c37a54..388a3ff55 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -56,11 +56,6 @@ val stm_debug : bool ref val profile : bool -(* Legacy flags *) - -(* -xml option: xml hooks will be called *) -val xml_export : bool ref - (* -ide_slave: printing will be more verbose, will affect stm caching *) val ide_slave : bool ref val ideslave_coqtop_flags : string option ref -- cgit v1.2.3