diff options
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | stm/vio_checking.ml | 7 |
2 files changed, 7 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build index b4be233faf..e683a6bda8 100644 --- a/Makefile.build +++ b/Makefile.build @@ -786,8 +786,6 @@ ifdef QUICK $(SHOW)'COQC -schedule-vio2vo $(NJOBS) theories/**.vio plugins/**.vio' $(HIDE)$(BOOTCOQC:-compile=-schedule-vio2vo) $(NJOBS) \ $(THEORIESVO) $(PLUGINSVO) - @# this should be done by -schedule-vio2vo, see #9334 - $(HIDE)touch $(THEORIESVO:.$(VO)=.vo) $(PLUGINSVO:.$(VO)=.vo) endif coqlib.timing.diff: theories.timing.diff plugins.timing.diff diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index 41e11ba255..69c1d9bd23 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -125,6 +125,7 @@ let schedule_vio_compilation j fs = | s :: rest -> s :: filter_argv b rest in let prog = Sys.argv.(0) in let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in + let all_jobs = !jobs in let make_job () = let f, t = List.hd !jobs in jobs := List.tl !jobs; @@ -141,6 +142,12 @@ let schedule_vio_compilation j fs = Worker.kill (Pool.find pid !pool); pool := Pool.remove pid !pool; done; + if !rc = 0 then begin + (* set the access and last modification time of all files to the same t + * not to confuse make into thinking that some of them are outdated *) + let t = Unix.gettimeofday () in + List.iter (fun (f,_) -> Unix.utimes (f^".vo") t t) all_jobs; + end; exit !rc |