diff options
| author | Pierre-Marie Pédrot | 2015-07-27 14:28:15 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-07-27 14:28:15 +0200 |
| commit | aff5a1aaeb9b50c60ff32b7d5336a44fd18428ee (patch) | |
| tree | 39d21c9798b9ce7fb59892414f71fb60be61bcde /dev | |
| parent | 05f22a5d6d5b8e3e80f1a37321708ce401834430 (diff) | |
| parent | cb145fa37d463210832c437f013231c9f028e1aa (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/vm_printers.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 4578a3b33d..3d688011c2 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -49,6 +49,7 @@ let rec ppzipper z = close_box() | Zfix _ -> print_string "Zfix" | Zswitch _ -> print_string "Zswitch" + | Zproj _ -> print_string "Zproj" and ppstack s = open_hovbox 0; |