From 09eeabb1182798c6381b478ff57fa429c281b35b Mon Sep 17 00:00:00 2001 From: wouter gordts Date: Thu, 4 Jul 2019 22:39:56 +0200 Subject: [PATCH] added git pull before the server starts --- web_server.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/web_server.py b/web_server.py index d7d073d..04b09de 100644 --- a/web_server.py +++ b/web_server.py @@ -40,6 +40,11 @@ def resources(filename): return bottle.static_file(filename, root="resources") def main(): + print("pulling latest github push") + status = subprocess.call(["git", "pull", "origin"]) + if status is not 0: + print("error pulling froom github...") + exit() print("generating FR doc now with pandoc") status = subprocess.call(["pandoc", "puredata_fr.md", "-o", "index_fr.html"]) print("generating EN doc now with pandoc")