diff options
Diffstat (limited to 'stm/vio_checking.ml')
| -rw-r--r-- | stm/vio_checking.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index 0f78e0acf6..cf0c8934b0 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -12,7 +12,7 @@ open Util let check_vio (ts,f_in) = Dumpglob.noglob (); - let _, _, _, _, tasks, _ = Library.load_library_todo f_in in + let _, _, _, tasks, _ = Library.load_library_todo f_in in Stm.set_compilation_hints f_in; List.fold_left (fun acc ids -> Stm.check_task f_in tasks ids && acc) true ts @@ -29,7 +29,7 @@ let schedule_vio_checking j fs = if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0"); let jobs = ref [] in List.iter (fun long_f_dot_vio -> - let _,_,_,_, tasks, _ = Library.load_library_todo long_f_dot_vio in + let _,_,_, tasks, _ = Library.load_library_todo long_f_dot_vio in Stm.set_compilation_hints long_f_dot_vio; let infos = Stm.info_tasks tasks in let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in |