From 9c1be9989be04f9be07a57ca51a0b250f7d9d332 Mon Sep 17 00:00:00 2001
From: Luigi Scarso <luigi.scarso@gmail.com>
Date: Sat, 19 Oct 2019 09:18:45 +0000
Subject: [PATCH] fixed build.sh script for WSL
[[Split portion of a mixed commit.]]
---
build-shared.sh | 2 ++
build.sh | 2 ++
2 files changed, 4 insertions(+)
diff --git a/build-shared.sh b/build-shared.sh
index 9eb77cac5..ad696c834 100755
--- a/build-shared.sh
+++ b/build-shared.sh
@@ -260,6 +260,8 @@ TL_MAKE=$MAKE ../source/configure $CONFHOST $CONFBUILD $WARNINGFLAGS\
--without-system-gd \
--without-system-libpng \
--without-system-poppler \
+ --without-system-gmp \
+ --without-system-mpfr \
--without-system-teckit \
--without-system-zlib \
--without-system-t1lib \
diff --git a/build.sh b/build.sh
index 10c203f59..4ac74cf6a 100755
--- a/build.sh
+++ b/build.sh
@@ -335,6 +335,8 @@ TL_MAKE=$MAKE ../source/configure $TEXLIVEOPT $CONFHOST $CONFBUILD $WARNINGFLA
--without-system-gd \
--without-system-libpng \
--without-system-poppler \
+ --without-system-gmp \
+ --without-system-mpfr \
--without-system-teckit \
--without-system-zlib \
--without-system-t1lib \
--
GitLab