diff options
| -rw-r--r-- | stdlib/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stdlib/Makefile b/stdlib/Makefile index cf11937c55..7031e2b433 100644 --- a/stdlib/Makefile +++ b/stdlib/Makefile @@ -252,7 +252,7 @@ $(OTHERS:.cmo=.cmi) std_exit.cmi: stdlib.cmi $(OBJS:.cmo=.cmx) std_exit.cmx: stdlib.cmi $(OBJS:.cmo=.p.cmx) std_exit.p.cmx: stdlib.cmi $(OTHERS:.cmo=.cmx) std_exit.cmx: stdlib.cmx -$(OTHERS:.cmo=.p.cmx) std_exit.p.cmx: stdlib.p.cmx +$(OTHERS:.cmo=.p.cmx) std_exit.p.cmx: stdlib.cmx clean:: rm -f *.cm* *.$(O) *.$(A) *.odoc |