Merge branch 'gostd-github' into gostd

jcburley · Apr 19, 2021 · a2bdc94 · a2bdc94
2 parents 26560d8 + fa312c0
commit a2bdc94
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/docs/dash.sh b/docs/dash.sh
@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 
 rm -f ./joker.xml
-../joker generate-xml.joke
+../joker generate-xml.joke || exit
 
 pushd dash
   rm -f ./*.html