diff options
Diffstat (limited to 'toplevel/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 48cd70f69..9f6f77ef1 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -41,7 +41,6 @@ let vernac_echo loc in_chan = let open Loc in (* vernac parses the given stream, executes interpfun on the syntax tree it * parses, and is verbose on "primitives" commands if verbosely is true *) -let chan_beautify = ref stdout let beautify_suffix = ".beautified" let set_formatter_translator ch = |