Add the gitlab mirrors.

[xonotic/xonotic.git] / misc / tools / all / config.subr

diff --git a/misc/tools/all/config.subr b/misc/tools/all/config.subr
index 1c560fa97c06777259ba058819ddef7023f9630a..fab9a3ffc6b8f3ae5c6956a3e68d0418f714831f 100644 (file)
--- a/misc/tools/all/config.subr
+++ b/misc/tools/all/config.subr
@@ -33,12 +33,23 @@ allmirrors()
        "$@" http nl   http://nl.git.xonotic.org/xonotic/  '*2'
 
        "$@" ssh  push ssh://xonotic@push.git.xonotic.org/ ''
        "$@" 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="time -p"
-if { $time sh -c 'true'; } 2>&1 >/dev/null | grep '^user ' >/dev/null; then
+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
        msg "Timing via the time utility works."
 else

-       time=
+       have_time=false

        msg "Timing not supported."
 fi
        msg "Timing not supported."
 fi