diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 0 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 |