diff options
Diffstat (limited to 'dev-ml/odns/files/odns-0.3-parmake.patch')
| -rw-r--r-- | dev-ml/odns/files/odns-0.3-parmake.patch | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/dev-ml/odns/files/odns-0.3-parmake.patch b/dev-ml/odns/files/odns-0.3-parmake.patch new file mode 100644 index 000000000000..7034abd25cf2 --- /dev/null +++ b/dev-ml/odns/files/odns-0.3-parmake.patch @@ -0,0 +1,16 @@ +fix parallel make +https://bugs.gentoo.org/show_bug.cgi?id=422683 + +Index: odns-0.3/OCamlMakefile +=================================================================== +--- odns-0.3.orig/OCamlMakefile ++++ odns-0.3/OCamlMakefile +@@ -1152,7 +1152,7 @@ $(BCDIDIR)/%.di $(NCDIDIR)/%.di: %.mli + $(DOC_DIR)/$(RESULT)/html: + mkdir -p $@ + +-$(DOC_DIR)/$(RESULT)/html/index.html: $(DOC_DIR)/$(RESULT)/html $(DOC_FILES) ++$(DOC_DIR)/$(RESULT)/html/index.html: $(DOC_DIR)/$(RESULT)/html $(DOC_FILES) byte-code-library + rm -rf $</* + $(QUIET)pp=`sed -n -e '/^#/d' -e 's/(\*pp \([^*]*\) \*)/\1/p;q' $(FIRST_DOC_FILE)`; \ + if [ -z "$$pp" ]; then \ |