From aee55acb375c6a5416481f741972d225617eaf47 Mon Sep 17 00:00:00 2001
From: Starbeamrainbowlabs <sbrl@starbeamrainbowlabs.com>
Date: Mon, 22 Jul 2019 15:24:15 +0100
Subject: [PATCH] Bugfix: Only write the development server PID file if it
 starts successfully

---
 build | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/build b/build
index f89015f..73bac6e 100755
--- a/build
+++ b/build
@@ -197,7 +197,7 @@ task_dev-server() {
 	task_begin "Starting development server";
 	php -S "[::1]:40482" &
 	exit_code=$?;
-	echo $! >/tmp/micro-lantern-dev-server.pid;
+	[[ "${exit_code}" -eq "0" ]] && echo $! >/tmp/micro-lantern-dev-server.pid;
 	task_end $?; # Should be 0 unless php died for some reason
 	sleep 1;
 }