]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/toplevel/top.ml
jet a change in dependences
[helm.git] / helm / software / helena / src / toplevel / top.ml
index 1d1de357295b8e29d5233d9549a638a0868688cc..b7c6fc1355c056329c416075b81d83953f4ea732 100644 (file)
@@ -403,7 +403,7 @@ let set_summary () =
 END
 
 let set_trace i = 
-   if !G.trace = 0 && i > 0 then Y.gmtime G.version_string;
+   if !G.trace = 0 && i > 0 then Y.gmtime (G.version_string false);
    if !G.trace > 0 && i = 0 then Y.utime_stamp "at exit";
    G.trace := i;
 IFDEF SUMMARY THEN
@@ -439,10 +439,11 @@ let main =
 (IFDEF QUOTE THEN "QUOTE" ELSE "" END);
 (IFDEF STAGE THEN "STAGE" ELSE "" END);
 (IFDEF TYPE THEN "TYPE" ELSE "" END);
+(IFDEF PROFV THEN "PROFV" ELSE "" END);
       ] in
       let map s = s <> "" in
       let features_string = KT.concat " " (KL.filter map features) in
-      L.warn level (KP.sprintf "%s [%s]" G.version_string features_string);
+      L.warn level (KP.sprintf "%s [%s]" (G.version_string true) features_string);
       exit 0
    in
    let set_hierarchy s = 
@@ -462,7 +463,7 @@ ELSE () END;
       streaming := false;
    in
    let undefined opt () =
-      L.warn level (KP.sprintf "%s was compiled without the support for option %s" G.version_string opt);
+      L.warn level (KP.sprintf "%s was compiled without the support for option %s" (G.version_string true) opt);
       exit 0
    in
    let arg_undefined opt = Arg.Unit (undefined opt) in