From 020ce9108bd995d9a842fa3651fe40764532cead Mon Sep 17 00:00:00 2001 From: Hanno Rein Date: Sat, 25 Jan 2025 21:54:13 +0000 Subject: [PATCH] cron-able documentation update --- docs/make_docs.bash | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/docs/make_docs.bash b/docs/make_docs.bash index 65b30bb43..621629ab3 100755 --- a/docs/make_docs.bash +++ b/docs/make_docs.bash @@ -1,4 +1,29 @@ #!/bin/bash +if [ -f documentation_lock.txt ]; then + echo "Documentation update already in progress. Exiting." + exit +fi +touch documentation_lock.txt + +git pull + +repository_head=` git rev-parse HEAD` +documentation_head=$( documentation_head.txt +rm documentation_lock.txt + +exit