From 1ea923e25ae8c2a0764eb41ffa5080edcea5d959 Mon Sep 17 00:00:00 2001
From: Yasin <mohammed-yasin.rahman@lip6.fr>
Date: Wed, 12 Feb 2014 14:37:08 +0100
Subject: [PATCH] Default port returned to 80

---
 devel/server-loop.sh | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/devel/server-loop.sh b/devel/server-loop.sh
index 1d94e8ee..c77258fc 100755
--- a/devel/server-loop.sh
+++ b/devel/server-loop.sh
@@ -3,7 +3,8 @@ DIRNAME=$(dirname $0)
 cd $DIRNAME/..
 
 # default port : if hostname starts with z -> use 8080 ; otherwise take 80
-hostname | grep -q '^z' && port=8080 || port=8080
+#hostname | grep -q '^z' && port=8080 || port=8080
+hostname | grep -q '^z' && port=8080 || port=80
 [[ -n "$@" ]] && port=$1
 
 while true; do 
-- 
2.43.0