commit 58b4e62a0def620769c926133843a0e60713eada
parent fee17638816e37c551e81ce72704dbb186f5e7bc
Author: finwo <finwo@pm.me>
Date: Tue, 21 Jul 2020 12:00:10 +0200
Prevent building alreay-built documents
Diffstat:
1 file changed, 5 insertions(+), 0 deletions(-)
diff --git a/build.sh b/build.sh
@@ -23,6 +23,11 @@ find ${ORGDIR} -maxdepth 1 -type d -regextype posix-egrep -regex '.*[0-9]{4}' |
script/template.sh -c ${spec}/data.ini src/html/index.html.entry >> docs/index.html
script/template.sh -c ${spec}/data.ini src/markdown/README.md.entry >> README.md
+ # Skip rendering already-existing files
+ if [ -f "${SPECDIR}/${DATA[identifier]}.pdf" ]; then
+ continue;
+ fi
+
# Check how to render the document itself
filename=$(echo ${spec}/document.*)
case "${filename##*.}" in