From ee1b5356826d367054b510b9b7e2956d2bc680b7 Mon Sep 17 00:00:00 2001
From: Frank Steinberg <steinberg@ibr.cs.tu-bs.de>
Date: Fri, 18 Oct 2019 13:37:05 +0200
Subject: [PATCH] Minor changes.
---
Makefile | 2 +-
web/save.cgi | 3 ++-
2 files changed, 3 insertions(+), 2 deletions(-)
diff --git a/Makefile b/Makefile
index ef2415c..29aca7c 100644
--- a/Makefile
+++ b/Makefile
@@ -84,7 +84,7 @@ distclean: clean
## Web Editor stuff -- this works only with additional manual adjustments
background:
- @nohup sh -c 'if [ ! -e .background ] ; then touch .background ; rm -f .background-again bjcp-2015-styleguide-de.xml web/bjcp-2015-styleguide-de.xml ; make ; rm .background ; if [ -e .background-again ] ; then rm bjcp-2015-styleguide-de.xml web/bjcp-2015-styleguide-de.xml ; make background ; fi ; else touch .background-again ; fi' >/dev/null 2>&1 &
+ @nohup sh -c 'if [ ! -e .background ] ; then touch .background ; rm -f .background-again bjcp-2015-styleguide-de.xml web/bjcp-2015-styleguide-de.xml ; make ; if [ -e .git-push ] ; then rm .git-push ; git push ; fi ; rm .background ; if [ -e .background-again ] ; then rm bjcp-2015-styleguide-de.xml web/bjcp-2015-styleguide-de.xml ; make background ; fi ; else touch .background-again ; fi' >/dev/null 2>&1 &
install-home:
ssh z "cd /var/www ; if [ -d bjcp-2015-styleguide ] ; then cd bjcp-2015-styleguide ; sudo -u www-data git pull ; sudo -u www-data make ; else sudo -u www-data git clone https://github.com/frsteinb/bjcp-2015-styleguide.git ; cd bjcp-2015-styleguide ; sudo -u www-data mkdir web/snippets ; sudo -u www-data make ; fi"
diff --git a/web/save.cgi b/web/save.cgi
index 292dc05..a435b70 100755
--- a/web/save.cgi
+++ b/web/save.cgi
@@ -151,7 +151,8 @@ if os.path.isfile(translatedfilename) or os.path.isfile(origfilename):
if os.path.isfile("/var/www/.ssh/id_rsa"):
log("pushing to GitHub repository")
- cmd = 'git push'
+ #cmd = 'git push'
+ cmd = 'touch .git-push'
docmd(cmd)
log("updating files in the background... otherwise done.")
--
GitLab