From b20d519c5ca19db16baa30c071fff306cd88d6cc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Wed, 11 May 2022 10:05:19 +0200
Subject: [PATCH] Fix build-manuals.sh renaming in release script
---
bin/build-src-distrib.sh | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/bin/build-src-distrib.sh b/bin/build-src-distrib.sh
index 81c5b820531..fa2215de1f2 100755
--- a/bin/build-src-distrib.sh
+++ b/bin/build-src-distrib.sh
@@ -728,7 +728,7 @@ case "${STEP}" in
step 1 "COMPILING PDF MANUALS"
run "rm -rf $MANUALS_DIR"
run "mkdir -p $MANUALS_DIR"
- run "$FILTER doc/build-manuals.sh"
+ run "$FILTER make -C doc all"
run "rm -rf $OUT_DIR/manuals"
run "mkdir -p $OUT_DIR/manuals"
run "cp $MANUALS_DIR/* $OUT_DIR/manuals"
--
GitLab