more robust extract-and-generate
This commit is contained in:
parent
f80a54a177
commit
d4082e602c
8
Makefile
8
Makefile
@ -5,6 +5,12 @@ SLIDES = slides-2021-03-29.pdf
|
||||
NON_ARCHIVABLES = notes.txt referatui.txt slides-2021-03-29.txt
|
||||
ARCHIVABLES = $(filter-out $(NON_ARCHIVABLES),$(shell git ls-files .))
|
||||
|
||||
ifeq ($(shell git rev-parse --is-inside-git-dir),true)
|
||||
GIT_DEP=$(shell git rev-parse --show-toplevel)/.git
|
||||
else
|
||||
GIT_DEP=
|
||||
endif
|
||||
|
||||
.PHONY: test
|
||||
test: tests.sql .faux.db
|
||||
./db -f tests.sql
|
||||
@ -64,7 +70,7 @@ $(SOURCE):
|
||||
wget http://download.geofabrik.de/europe/$@
|
||||
|
||||
REF = $(shell git describe --abbrev=12 --always --dirty)
|
||||
version.tex: Makefile $(shell git rev-parse --show-toplevel)/.git
|
||||
version.tex: Makefile $(GIT_DEP)
|
||||
( \
|
||||
TZ=UTC date '+\gdef\VCDescribe{%F ($(REF))}%'; \
|
||||
) > $@
|
||||
|
@ -1,19 +1,15 @@
|
||||
#!/bin/bash
|
||||
set -euo pipefail
|
||||
|
||||
fail() {
|
||||
>&2 echo "$1"
|
||||
exit 1
|
||||
}
|
||||
|
||||
dir=$(mktemp -d)
|
||||
fname=mj-msc-all.pdf
|
||||
|
||||
echo "Extracting all files from the report ..."
|
||||
pdfdetach -saveall -o "$dir" mj-msc-all.pdf
|
||||
echo "Extracting all files from the report to $dir ..."
|
||||
pdfdetach -saveall -o "$dir" "$fname"
|
||||
|
||||
echo "Re-generating the report..."
|
||||
echo "Generating $dir/$fname..."
|
||||
fail=0
|
||||
make -C "$dir" -j $(nproc) mj-msc-all.pdf 2>&1 > make.log || fail=1
|
||||
make -C "$dir" -j $(nproc) "$fname" > "$dir/make.log" 2>&1 || fail=1
|
||||
|
||||
if [[ $fail == 1 ]]; then
|
||||
>&2 echo "Generation failed. Here are the last 10 log lines:"
|
||||
@ -22,7 +18,10 @@ if [[ $fail == 1 ]]; then
|
||||
fi
|
||||
|
||||
open=open
|
||||
if [[ $(uname) == Linux ]]
|
||||
open=xdg-open
|
||||
fi
|
||||
"$open" "$dir/mj-msc-all.pdf"
|
||||
[[ $(uname) == Linux ]] && open=xdg-open
|
||||
|
||||
echo "Opening $dir/$fname ..."
|
||||
"$open" "$dir/$fname"
|
||||
|
||||
echo "Editor has been closed. Removing $dir"
|
||||
rm -fr "$dir"
|
||||
|
Loading…
Reference in New Issue
Block a user