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. --- library/library.mli | 3 --- 1 file changed, 3 deletions(-) (limited to 'library/library.mli') diff --git a/library/library.mli b/library/library.mli index 604167804..6c624ce52 100644 --- a/library/library.mli +++ b/library/library.mli @@ -67,9 +67,6 @@ val library_full_filename : DirPath.t -> string (** - Overwrite the filename of all libraries (used when restoring a state) *) val overwrite_library_filenames : string -> unit -(** {6 Hook for the xml exportation of libraries } *) -val xml_require : (DirPath.t -> unit) Hook.t - (** {6 Locate a library in the load paths } *) exception LibUnmappedDir exception LibNotFound -- cgit v1.2.3