diff options
Diffstat (limited to 'lib/pp.ml4')
| -rw-r--r-- | lib/pp.ml4 | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/lib/pp.ml4 b/lib/pp.ml4 index 7f0def529..91a99b5fb 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -183,7 +183,6 @@ let rec pr_com ft s = (* pretty printing functions *) let pp_dirs ft = - let maxbox = (get_gp ft).max_depth in let pp_open_box = function | Pp_hbox n -> Format.pp_open_hbox ft () | Pp_vbox n -> Format.pp_open_vbox ft n |