diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index 3887dfdec7..38cdd53be6 100644 --- a/Makefile.build +++ b/Makefile.build @@ -849,7 +849,7 @@ endif $(SHOW)'CCDEP $<' $(HIDE)$(CC) -MM -MG -MQ "$@" -MQ "$(<:.c=.o)" $(CFLAGS) $(CINCLUDES) $< > $@ -.PRECIOUS: %.ml %.mli %.d %.ml4.d kernel/copcodes.ml +.SECONDARY: $(GENFILES) ########################################################################### # this sets up developper supporting stuff |