aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/dumpglob.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/dumpglob.ml')
-rw-r--r--interp/dumpglob.ml5
1 files changed, 2 insertions, 3 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 519f902ba..702c509dc 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -212,6 +212,5 @@ let dump_notation_location posl df (((path,secpath),_),sc) =
let secpath = Names.string_of_dirpath secpath in
let df = cook_notation df sc in
List.iter (fun (bl,el) ->
- for pos=bl to el do
- dump_string (Printf.sprintf "R%d %s %s %s not\n" pos path secpath df)
- done) posl
+ dump_string(Printf.sprintf "R%d:%d %s %s %s not\n" bl el path secpath df))
+ posl