diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-08 22:02:12 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-09 08:13:18 +0200 |
| commit | 25b0a871bde109788492992f1cb417e7e163ffa3 (patch) | |
| tree | ac05ee99faa7368f4eaf98e275a594bddfc6dfb0 /toplevel | |
| parent | 82eb6cbfa3db53756ea40fb4795836d6f8c55bbe (diff) | |
Fixing beautification to file.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 55f3a31a3..bdd834d52 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -132,7 +132,7 @@ let pr_new_syntax loc ocom = | Some com -> Ppvernac.pr_vernac com | None -> mt() in if !beautify_file then - Feedback.msg_notice (hov 0 (comment (fst loc) ++ com ++ comment (snd loc))) + Pp.msg_with !Pp_control.std_ft (hov 0 (comment (fst loc) ++ com ++ comment (snd loc))) else Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com))); States.unfreeze fs; |