X-Git-Url: https://git.xonotic.org/?p=xonotic%2Fxonotic.git;a=blobdiff_plain;f=misc%2Ftools%2Fall%2Fconfig.subr;h=fab9a3ffc6b8f3ae5c6956a3e68d0418f714831f;hp=cb07d15ea8c1f8e24f00e07c63fb6f6cdb8775f0;hb=09a070cf39121ed5443b9dd7b169d47ced1ea37b;hpb=521c08406137d3ea1c92fcf401430306166c4b50

diff --git a/misc/tools/all/config.subr b/misc/tools/all/config.subr
index cb07d15e..fab9a3ff 100644
--- a/misc/tools/all/config.subr
+++ b/misc/tools/all/config.subr
@@ -33,9 +33,23 @@ allmirrors()
 	"$@" http nl   http://nl.git.xonotic.org/xonotic/  '*2'
 
 	"$@" ssh  push ssh://xonotic@push.git.xonotic.org/ ''
+
+	"$@" http lab  https://gitlab.com/xonotic/         ''
+	"$@" ssh  lab  ssh://git@gitlab.com/xonotic/       ''
 }
 
-time=
-if { time -p sh -c 'true'; } 2>&1 >/dev/null | grep '^user ' >/dev/null; then
-	time="time -p"
+have_time=true
+measure_time()
+{
+	if $have_time; then
+		time -p "$@"
+	else
+		"$@"
+	fi
+}
+if { measure_time sh -c 'true'; } 2>&1 >/dev/null | grep '^user ' >/dev/null; then
+	msg "Timing via the time utility works."
+else
+	have_time=false
+	msg "Timing not supported."
 fi