From 183c64eb0f640c360a3aee97f8e97b8b1cebca98 Mon Sep 17 00:00:00 2001
From: "Achim D. Brucker" <adbrucker@0x5f.org>
Date: Sat, 20 Jul 2019 15:34:16 +0100
Subject: [PATCH] Moved build script into separate directory.

---
 document-generator/{document-template => scripts}/build        | 0
 document-generator/{document-template => scripts}/build_lib.sh | 0
 install                                                        | 1 +
 3 files changed, 1 insertion(+)
 rename document-generator/{document-template => scripts}/build (100%)
 rename document-generator/{document-template => scripts}/build_lib.sh (100%)

diff --git a/document-generator/document-template/build b/document-generator/scripts/build
similarity index 100%
rename from document-generator/document-template/build
rename to document-generator/scripts/build
diff --git a/document-generator/document-template/build_lib.sh b/document-generator/scripts/build_lib.sh
similarity index 100%
rename from document-generator/document-template/build_lib.sh
rename to document-generator/scripts/build_lib.sh
diff --git a/install b/install
index 2fa10f6..59f613b 100755
--- a/install
+++ b/install
@@ -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"