2022-02-15 21:46:39 +01:00
|
|
|
set -e
|
|
|
|
|
echo "Building document"
|
|
|
|
|
make pdf
|
|
|
|
|
mkdir public
|
2022-02-15 23:46:02 +01:00
|
|
|
mv build/$mainfile.pdf public
|
|
|
|
|
mv build/$mainfile.log public
|
2022-02-15 21:46:39 +01:00
|
|
|
cd public/
|
2022-02-15 23:46:02 +01:00
|
|
|
tree -H '.' -I "index.html" -D --charset utf-8 -T "$course" > index.html
|
