aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/util.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/util.ml b/lib/util.ml
index c733ed3335..dd5be58714 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -480,7 +480,7 @@ let prvecti elem v =
else
let r = pr (i-1) and e = elem i v.(i) in [< r; e >]
in
- pr (n-1)
+ if n=0 then [< >] else pr (n - 1)
let prvect_with_sep sep elem v =
let rec pr n =