aboutsummaryrefslogtreecommitdiff
path: root/toplevel/vi_checking.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/vi_checking.ml')
-rw-r--r--toplevel/vi_checking.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vi_checking.ml b/toplevel/vi_checking.ml
index 37f4266d04..cb6e601362 100644
--- a/toplevel/vi_checking.ml
+++ b/toplevel/vi_checking.ml
@@ -11,7 +11,7 @@ open Util
let check_vi (ts,f) =
Dumpglob.noglob ();
let long_f_dot_v, _, _, _, tasks, _ = Library.load_library_todo f in
- Stm.set_compilation_hints (Aux_file.load_aux_file_for long_f_dot_v);
+ Stm.set_compilation_hints long_f_dot_v;
List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts
module Worker = Spawn.Sync(struct
@@ -39,7 +39,7 @@ let schedule_vi_checking j fs =
if Filename.check_suffix f ".vi" then Filename.chop_extension f
else f in
let long_f_dot_v, _,_,_, tasks, _ = Library.load_library_todo f in
- Stm.set_compilation_hints (Aux_file.load_aux_file_for long_f_dot_v);
+ Stm.set_compilation_hints long_f_dot_v;
let infos = Stm.info_tasks tasks in
let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in
if infos <> [] then jobs := (f, eta, infos) :: !jobs)