aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/modintern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/modintern.ml')
-rw-r--r--interp/modintern.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/interp/modintern.ml b/interp/modintern.ml
index cd55ec74d..0af11bad9 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -76,7 +76,6 @@ let split_modpath mp =
let dump_moddef loc mp ty =
if !Flags.dump then
let (dp, l) = split_modpath mp in
- let fp = string_of_dirpath dp in
let mp = string_of_dirpath (make_dirpath l) in
Flags.dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (unloc loc)) "<>" mp)