1. MatitaGuiTypes.gui interface streamlined

[helm.git] / matita / matita / matitaScript.mli

diff --git a/matita/matita/matitaScript.mli b/matita/matita/matitaScript.mli
index add51ccf02eb6e88060fd848b5b79b1d42ef9794..81ade1c88c34ec0e8a87bfef61920ad0d3b128bb 100644 (file)
--- a/matita/matita/matitaScript.mli
+++ b/matita/matita/matitaScript.mli
@@ -109,6 +109,7 @@ val script:
   unit -> 
     script
 
+val destroy: int -> unit
 val current: unit -> script
 val at_page: int -> script
 val iter_scripts: (script -> unit) -> unit