summaryrefslogtreecommitdiff
path: root/lib/aux_file.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:43:34 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:43:34 +0100
commit4e76c4f01b69b77f40686e06c4544aa156efaa5a (patch)
treeaefad2e3de35f75c46729f9310d33b56d3821961 /lib/aux_file.ml
parent64fa31c7ee53e79b112507fb2eea27dc7648328d (diff)
parent91dbeab8eef959c3f64960909ca69d4e68c8198d (diff)
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'lib/aux_file.ml')
-rw-r--r--lib/aux_file.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index c9018c9e..5dedb0d0 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -42,6 +42,8 @@ module M = Map.Make(String)
type data = string M.t
type aux_file = data H.t
+let contents x = x
+
let empty_aux_file = H.empty
let get aux loc key = M.find key (H.find (Loc.unloc loc) aux)