Moved build script into separate directory.

This commit is contained in:
Achim D. Brucker 2019-07-20 15:34:16 +01:00
parent e6cea1156c
commit 183c64eb0f
3 changed files with 1 additions and 0 deletions

View File

@ -179,6 +179,7 @@ install_and_register(){
DIR="$ISABELLE_HOME_USER/DOF/document-template"
echo " - Installing document templates in $DIR"
mkdir -p "$DIR"
cp $GEN_DIR/scripts/* "$DIR"
cp $GEN_DIR/document-template/* "$DIR"
DIR="$ISABELLE_HOME_USER/DOF/latex"