changeset 6324:6c9d803d4a83

* src/mpfr.mk: remove docs
author John Donoghue <john.donoghue@ieee.org>
date Wed, 20 Jul 2022 09:05:59 -0400
parents d44081b8cc2a
children ad7b12d96767
files src/mpfr.mk
diffstat 1 files changed, 5 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/mpfr.mk	Wed Jul 20 08:50:41 2022 -0400
+++ b/src/mpfr.mk	Wed Jul 20 09:05:59 2022 -0400
@@ -26,6 +26,9 @@
         --enable-threads=win32 \
         --with-gmp-include='$(HOST_INCDIR)'
         --with-gmp-lib='$(HOST_LIBDIR)'
-    $(MAKE) -C '$(1)' -j '$(JOBS)'
-    $(MAKE) -C '$(1)' -j '$(JOBS)' install
+    $(MAKE) -C '$(1)' -j '$(JOBS)' $(MXE_DISABLE_DOCS)
+    $(MAKE) -C '$(1)' -j '$(JOBS)' $(MXE_DISABLE_DOCS) install DESTDIR='$(3)'
+    if [ "$(ENABLE_DEP_DOCS)" == "no" ]; then \
+       rm -rf "$(3)$(HOST_PREFIX)/share/doc/mpfr"; \
+    fi
 endef