aboutsummaryrefslogtreecommitdiffstats
path: root/debug
diff options
context:
space:
mode:
Diffstat (limited to 'debug')
-rw-r--r--debug/DebugInformation.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml
index 12ae835b..36138882 100644
--- a/debug/DebugInformation.ml
+++ b/debug/DebugInformation.ml
@@ -521,6 +521,7 @@ let add_lvar_scope f_id var_id s_id =
with Not_found -> ()
let insert_local_declaration sto id ty loc =
+ add_file (fst loc);
let ty = insert_type ty in
let var = {
lvar_name = id.name;
@@ -691,6 +692,6 @@ let init name =
Hashtbl.reset compilation_section_start;
Hashtbl.reset compilation_section_end;
Hashtbl.reset filenum;
+ all_files := StringSet.singleton name;
Hashtbl.reset diab_additional;
- all_files := StringSet.empty;
printed_vars := StringSet.empty;