X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Ftoplevel%2Ftop.ml;h=b7c6fc1355c056329c416075b81d83953f4ea732;hb=fdb80b08af83b86759833142456ce3c4f84cd80e;hp=1d1de357295b8e29d5233d9549a638a0868688cc;hpb=586c361209ac14e8c2b1da3509041c0c82a86c92;p=helm.git

diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml
index 1d1de3572..b7c6fc135 100644
--- a/helm/software/helena/src/toplevel/top.ml
+++ b/helm/software/helena/src/toplevel/top.ml
@@ -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