X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fprobe%2Foptions.ml;h=0b9487d6bf68d6d15ed8f4faba317b4ae76fa54c;hp=ce29c1ef0f7499b6e9e16b8b4275865c3a4f6fd0;hb=076439def28e649ec384fae038ed021dadd5f75c;hpb=d2545ffd201b1aa49887313791386add78fa8603

diff --git a/matita/components/binaries/probe/options.ml b/matita/components/binaries/probe/options.ml
index ce29c1ef0..0b9487d6b 100644
--- a/matita/components/binaries/probe/options.ml
+++ b/matita/components/binaries/probe/options.ml
@@ -1,12 +1,12 @@
 (*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.      
-     \ /   This software is distributed as is, NO WARRANTY.     
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department, University of Bologna, Italy.
+    ||I||
+    ||T||  HELM is free software; you can redistribute it and/or
+    ||A||  modify it under the terms of the GNU General Public License
+    \   /  version 2 or (at your option) any later version.
+     \ /   This software is distributed as is, NO WARRANTY.
       V_______________________________________________________________ *)
 
 module A = Array
@@ -44,6 +44,8 @@ let default_objs = US.empty
 
 let default_srcs = US.empty
 
+let default_names = US.empty
+
 let default_remove = []
 
 let default_exclude = []
@@ -66,6 +68,8 @@ let objs = ref default_objs
 
 let srcs = ref default_srcs
 
+let names = ref default_names
+
 let remove = ref default_remove
 
 let exclude = ref default_exclude
@@ -113,8 +117,8 @@ let out_deps file =
 
 let clear () =
   R.clear (); A.iteri clear_slot slot;
-  objs := default_objs; srcs := default_srcs; remove := default_remove;
-  exclude := default_exclude; net := default_net;
+  objs := default_objs; srcs := default_srcs; names := default_names;
+  remove := default_remove; exclude := default_exclude; net := default_net;
   chars := default_chars; debug_lexer := default_debug_lexer;
   no_devel := default_no_devel; no_init := default_no_init;
   deps := UPS.empty