From 9d55a431cfd48db4a09ef3f103c9595c8e0eb463 Mon Sep 17 00:00:00 2001
From: Jannik Dreier <jannik.dreier@loria.fr>
Date: Mon, 17 Jul 2023 14:37:40 +0200
Subject: [PATCH] deploy develop manual

---
 deploy.sh  | 27 ++++++++++++++-------------
 index.html | 18 +++++++++++++++++-
 2 files changed, 31 insertions(+), 14 deletions(-)

diff --git a/deploy.sh b/deploy.sh
index 1bf48e9..5f674e0 100755
--- a/deploy.sh
+++ b/deploy.sh
@@ -2,11 +2,13 @@
 set -e # Exit with nonzero exit code if anything fails
 
 # Set up some git information.
-REPO=`git config remote.origin.url`
+REPO=`git config remote.${1:=origin}.url`
 SSH_REPO=${REPO/https:\/\/github.com\//git@github.com:}
 SHA=`git rev-parse --verify HEAD`
+BRANCH=`git rev-parse --abbrev-ref HEAD`
 
-SOURCE_BRANCH="master"
+MASTER_BRANCH="master"
+DEVELOP_BRANCH="develop"
 TARGET_BRANCH="gh-pages"
 
 function doCompile {
@@ -14,11 +16,10 @@ function doCompile {
     make pdf
 }
 
-# Pull requests and commits to other branches shouldn't try to deploy, just build to verify
-#if [ "$TRAVIS_PULL_REQUEST" != "false" -o "$TRAVIS_BRANCH" != "$SOURCE_BRANCH" ]; then
-#    echo "Skipping deploy; not the right kind of build."
-#    exit 0
-#fi
+if [ [$BRANCH != $MASTER_BRANCH] -o [$BRANCH != $DEVELOP_BRANCH] ]; then
+    echo "Please use this script on branch $MASTER_BRANCH or $DEVELOP_BRANCH only. You seem to be on $BRANCH."
+    exit 0
+fi
 
 # Clone the existing gh-pages for this repo into a temporary folder $CHECKOUT.
 CHECKOUT=`mktemp -d`
@@ -29,15 +30,15 @@ git -C $CHECKOUT config user.email "$COMMIT_AUTHOR_EMAIL"
 git -C $CHECKOUT checkout $TARGET_BRANCH || git -C $CHECKOUT checkout --orphan $TARGET_BRANCH
 
 # Replace existing contents of checkout with the results of a fresh compile.
-rm -rf $CHECKOUT/* || exit 0
+rm -rf $CHECKOUT/$BRANCH || exit 0
+mkdir -p $CHECKOUT/$BRANCH/tex
 doCompile
 for x in book code code_ERRORexamples code_ObsEquiv images
 do
-    cp -r $x $CHECKOUT
+    cp -r $x $CHECKOUT/$BRANCH
 done
-mkdir -p $CHECKOUT/tex
-cp tex/tamarin-manual.pdf $CHECKOUT/tex/tamarin-manual.pdf
-cp index.html $CHECKOUT/index.html
+cp tex/tamarin-manual.pdf $CHECKOUT/$BRANCH/tex/tamarin-manual.pdf
+cp index.html $CHECKOUT/$BRANCH/index.html
 
 # If there are no changes to the compiled book (e.g. this is a README update) then just bail.
 if [[ -z `git -C $CHECKOUT status --porcelain` ]]; then
@@ -47,7 +48,7 @@ fi
 
 # Commit the "changes", i.e. the new version. The delta will show diffs between new and old versions.
 git -C $CHECKOUT add \*
-git -C $CHECKOUT commit -m "Deploy to GitHub Pages: ${SHA}"
+git -C $CHECKOUT commit -m "Deploy to GitHub Pages on ${BRANCH}: ${SHA}"
 
 # Get the deploy key by using Githubs's stored variables to decrypt deploy_key.enc.
 openssl enc -nosalt -aes-256-cbc -d -in deploy_key.enc -out deploy_key -base64 -K $ENCRYPTED_KEY -iv $ENCRYPTED_IV
diff --git a/index.html b/index.html
index df8f74f..25c52db 100644
--- a/index.html
+++ b/index.html
@@ -22,7 +22,23 @@
     <div id='page'>
 <h1>Welcome to the Tamarin Manual</h1>
 <p class="halfbreak">
-The manual is available as a <a href='tex/tamarin-manual.pdf'>PDF</a> or as <a href='book/001_introduction.html'>HTML</a> for online browsing.
+The manual is available as a
+<a href='master/tex/tamarin-manual.pdf'>PDF</a>
+or as 
+<a href='master/book/001_introduction.html'>HTML</a>
+for online browsing. 
+</p>
+
+<p style="font-size: smaller">
+(For developers and others who are working with the 
+<a href="https://github.com/tamarin-prover/tamarin-prover/tree/develop">
+    development branch
+</a>
+of Tamarin: see here for the
+<a href='develop/tex/tamarin-manual.pdf'>PDF</a>
+and
+<a href='develop/book/001_introduction.html'>HTML</a>
+in sync with <tt>develop</tt>.)
 </p>
     </div>
   </div>