diff options
| author | Enrico Tassi | 2019-01-11 11:46:47 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-01-11 11:50:25 +0100 |
| commit | 44b5f77f36011e797f0d7d36098296dc7d6c1c51 (patch) | |
| tree | 7c98f3b6cec9d7e81371183fa775816484b87960 | |
| parent | 325f7ffb27496c8017d50712fe100658ea39bf2b (diff) | |
[STM] set the mtime of files generated via vio2vo (fix #9334)
| -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 |