aboutsummaryrefslogtreecommitdiffhomepage
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 a52a83dfe..5fae1c459 100644
--- a/toplevel/vi_checking.ml
+++ b/toplevel/vi_checking.ml
@@ -10,7 +10,7 @@ open Util
let check_vi (ts,f) =
Dumpglob.noglob ();
- let tasks, long_f_dot_v = Library.load_library_todo 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);
List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts
@@ -38,7 +38,7 @@ let schedule_vi_checking j fs =
let f =
if Filename.check_suffix f ".vi" then Filename.chop_extension f
else f in
- let tasks, long_f_dot_v = Library.load_library_todo 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);
let infos = Stm.info_tasks tasks in
let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in