diff options
Diffstat (limited to 'otherlibs/threads/Makefile')
| -rw-r--r-- | otherlibs/threads/Makefile | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/otherlibs/threads/Makefile b/otherlibs/threads/Makefile index af89857497..d2cda03319 100644 --- a/otherlibs/threads/Makefile +++ b/otherlibs/threads/Makefile @@ -94,10 +94,10 @@ marshal.cmi: $(LIB)/marshal.cmi ln -s $(LIB)/marshal.cmi marshal.cmi unix.mli: $(UNIXLIB)/unix.mli - ln -sf $(UNIXLIB)/unix.mli unix.mli + ln -s -f $(UNIXLIB)/unix.mli unix.mli unix.cmi: $(UNIXLIB)/unix.cmi - ln -sf $(UNIXLIB)/unix.cmi unix.cmi + ln -s -f $(UNIXLIB)/unix.cmi unix.cmi unix.cmo: unix.mli unix.cmi $(UNIXLIB)/unixLabels.cmo $(CAMLC) ${COMPFLAGS} -c unix.ml |