Clean up script a bit, don't use a predefined copy of the git repo.

Author: eldering

update_docs.sh

@@ -1,24 +1,29 @@
-#!/bin/bash -ex
+#!/bin/sh -e
 
-DOC_REPO=/home/domjudge/doc_update/doc_repo
 WEBSERVER_PATH=/srv/http/domjudge/docs/manual
 JSON="${WEBSERVER_PATH}/versions.json"
 
+TMPDIR=$(mktemp -d -t 'update_docs-XXXXXX')
+DOC_REPO="$TMPDIR/domjudge"
+git clone https://github.com/DOMjudge/domjudge.git "$DOC_REPO"
+
 for version in `cat "${JSON}" | jq -r -c '.[]'`; do
 	rm -rf "${WEBSERVER_PATH}/${version}"
 	mkdir -p "${WEBSERVER_PATH}/${version}"
 	(
-	  cd "${DOC_REPO}"
-	  git stash
-	  git checkout "${version}"
-	  git pull
-	  rm -rf doc/manual/build/html/
-	  if [ "$version" = "main" ]; then
-		  sed -i -e "s/^version.*/version = 'main'/" doc/manual/version.py.in
-	  fi
-	  ./bootstrap
-	  ./configure
-	  make docs
-	  cp -r doc/manual/build/html/* "${WEBSERVER_PATH}/${version}/"
+		cd "$DOC_REPO"
+		git reset --hard HEAD
+		git clean -df
+		git checkout "$version"
+		rm -rf doc/manual/build/html/
+		if [ "$version" = "main" ]; then
+			sed -i -e "s/^version.*/version = 'main'/" doc/manual/version.py.in
+		fi
+		./bootstrap
+		./configure
+		make docs
+		cp -r doc/manual/build/html/* "${WEBSERVER_PATH}/${version}/"
 	)
 done
+
+rm -rf "$TMPDIR"