From 9225c03547f9752b4a495e2db0fd3ef783af9f2b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maximilian=20Ke=C3=9Fler?= Date: Thu, 19 Oct 2023 10:55:10 +0200 Subject: [PATCH] remove unneded script --- .ci/compile_doc.sh | 9 --------- 1 file changed, 9 deletions(-) delete mode 100755 .ci/compile_doc.sh diff --git a/.ci/compile_doc.sh b/.ci/compile_doc.sh deleted file mode 100755 index 6b32f75..0000000 --- a/.ci/compile_doc.sh +++ /dev/null @@ -1,9 +0,0 @@ -set -e - -# set up packages to be available for latex -mkdir -p ~/texmf/tex/latex -ln -s build/packages ~/texmf/tex/latex/packages - -# generate doc -make doc -