From e289037379af0496be00eb8e0412edbaf1c32e17 Mon Sep 17 00:00:00 2001 From: Michael Young Date: Wed, 5 Mar 2025 16:58:42 +0000 Subject: [PATCH] Allow user packages in make doc --- doc/make_doc.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/make_doc.in b/doc/make_doc.in index ac535332e4..dafe4479c2 100644 --- a/doc/make_doc.in +++ b/doc/make_doc.in @@ -4,7 +4,7 @@ set -e set -o pipefail GAP=@abs_top_builddir@/gap -GAPARGS="-b -m 1g -x 80 -q --quitonbreak -r" +GAPARGS="-b -m 1g -x 80 -q --quitonbreak" if [ "$1" == "nopdf" ]; then NOPDF=", \"nopdf\"" else