diff options
Diffstat (limited to 'dev/vm_printers.ml')
| -rw-r--r-- | dev/vm_printers.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 11565b99eb..73cf1b0195 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -51,7 +51,7 @@ let rec ppzipper z = let n = nargs args in open_hbox (); for i = 0 to n-2 do - ppvalues (arg args i);print_string ";";print_space() + ppvalues (arg args i);print_string ";";print_space() done; if n-1 >= 0 then ppvalues (arg args (n-1)); close_box() |