1 files changed, 1 insertions, 1 deletions
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 7777d091..569a028f 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -279,7 +279,7 @@ let pp_dirs ft =
     try
       Stream.iter pp_dir dirstream; com_brk ft
     with
-      | e -> Format.pp_print_flush ft () ; raise e
+      | reraise -> Format.pp_print_flush ft () ; raise reraise
 
 
 (* pretty print on stdout and stderr *)