diff options
| -rw-r--r-- | ocamldoc/Makefile | 2 | ||||
| -rw-r--r-- | ocamldoc/runocamldoc | 11 |
2 files changed, 12 insertions, 1 deletions
diff --git a/ocamldoc/Makefile b/ocamldoc/Makefile index 6a1e4b845..7f76a1906 100644 --- a/ocamldoc/Makefile +++ b/ocamldoc/Makefile @@ -32,7 +32,7 @@ OCAMLPP=-pp 'grep -v DEBUG' MKDIR=mkdir -p CP=cp -f OCAMLDOC=ocamldoc -OCAMLDOC_RUN=$(CAMLRUN) -I ../otherlibs/unix -I ../otherlibs/str ./$(OCAMLDOC) +OCAMLDOC_RUN=sh ./runocamldoc $(SUPPORTS_SHARED_LIBRARIES) OCAMLDOC_OPT=$(OCAMLDOC).opt OCAMLDOC_LIBCMA=odoc_info.cma OCAMLDOC_LIBCMI=odoc_info.cmi diff --git a/ocamldoc/runocamldoc b/ocamldoc/runocamldoc new file mode 100644 index 000000000..0f6878f14 --- /dev/null +++ b/ocamldoc/runocamldoc @@ -0,0 +1,11 @@ +#!/bin/sh + +case "$1" in + true) shift + exec ../ocamlrun -I ../otherlibs/unix -I ../otherlibs/str ./ocamldoc $* + ;; + *) shift + exec ./ocamldoc $* + ;; +esac +
\ No newline at end of file |