diff options
Diffstat (limited to 'toplevel/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index b7d34070a..3562acd7a 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -111,8 +111,8 @@ let rec vernac interpfun input = let tstart = System.get_time() in interp v; let tend = System.get_time() in - mSGNL [< 'sTR"Finished transaction in " ; - System.fmt_time_difference tstart tend >] + msgnl (str"Finished transaction in " ++ + System.fmt_time_difference tstart tend) | _ -> if not !just_parsing then interpfun com in |