From bdf3d6615e66ef6de4d21a5e464c472723617289 Mon Sep 17 00:00:00 2001
From: darkgrin <darkgrin@yahoo.com>
Date: Tue, 1 Apr 2014 00:38:33 +0800
Subject: [PATCH] Fix error "Undefined index: SERVER_ADDR". This is
 reproducible when we use php's built in server via 'php -S ...'.

---
 editor.php | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/editor.php b/editor.php
index ffc09ef..6587d75 100644
--- a/editor.php
+++ b/editor.php
@@ -70,7 +70,7 @@ h2 {color: rgba(0,198,255,0.7)}
 	<div style="float: left; width: 300px; margin-right: 50px">
 		<h2>server</h2>
 		<span class="heading">Server name, OS & IP:</span><br>
-		<?php echo $_SERVER['SERVER_NAME']." &nbsp;&nbsp ".$_SERVER['SERVER_SOFTWARE']." &nbsp;&nbsp ".$_SERVER['SERVER_ADDR'];?><br><br>
+		<?php echo $_SERVER['SERVER_NAME']." &nbsp;&nbsp ".$_SERVER['SERVER_SOFTWARE']." &nbsp;&nbsp ".(isset($_SERVER['SERVER_ADDR'])?$_SERVER['SERVER_ADDR']:"Unknown");?><br><br>
 		<span class="heading">Root:</span><br>
 		<?php echo $docRoot;?><br><br>
 		<span class="heading">ICEcoder root:</span><br>
@@ -316,4 +316,4 @@ var debounce;
 
 </body>
 
-</html>
\ No newline at end of file
+</html>