From 163742029c14abdce0be94bbaba903039080fc0b Mon Sep 17 00:00:00 2001
From: pi-rho <github@tyr.cx>
Date: Fri, 15 Sep 2017 10:18:13 -0600
Subject: [PATCH] posixify devel.sh in case someone wants to run this on a
 wristwatch or a poorly designed box that doesn't have modern bash

---
 devel.sh | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/devel.sh b/devel.sh
index 86675e9..d79d263 100755
--- a/devel.sh
+++ b/devel.sh
@@ -1,8 +1,10 @@
-#!/bin/bash -e
+#!/bin/sh
 #
 # Script to clone and start a development server
 
-if [[ -f tools/devel-server.py ]]; then
+set -e
+
+if [ -f tools/devel-server.py ]; then
 	cat <<EOM
 This script is intended to be used to bootstrap a moth development server. It
 looks like you're running the script from a moth repository working directory.
@@ -14,8 +16,8 @@ EOM
 	exit 1
 fi
 
-[[ -d puzzles  ]] || mkdir -p puzzles
-[[ -d moth/bin ]] || git clone https://github.com/dirtbags/moth.git
+[ -d puzzles  ] || mkdir -p puzzles
+[ -d moth/bin ] || git clone https://github.com/dirtbags/moth.git
 
 cd moth
 puzzles="$(readlink -e ../puzzles)"