devsite_url="http://dev.xonotic.org/" gitsite_url="http://gitlab.com/groups/xonotic/" allrepos() { "$@" . xonotic.git master "" "$@" data/xonotic-data.pk3dir xonotic-data.pk3dir.git master "" "$@" data/xonotic-music.pk3dir xonotic-music.pk3dir.git master "" "$@" data/xonotic-nexcompat.pk3dir xonotic-nexcompat.pk3dir.git master "no" "$@" darkplaces darkplaces.git div0-stable "svn" "$@" netradiant netradiant.git master "" "$@" div0-gittools div0-gittools.git master "no" "$@" d0_blind_id d0_blind_id.git master "" "$@" data/xonotic-maps.pk3dir xonotic-maps.pk3dir.git master "" "$@" mediasource mediasource.git master "no" "$@" gmqcc gmqcc.git master "" "$@" xonstat xonstat.git master "no" "$@" xonstatdb xonstatdb.git master "no" } allmirrors() { # Legacy git URLs. "$@" git '' git://git.xonotic.org/xonotic/ '' "$@" http '' http://git.xonotic.org/xonotic/ '' "$@" ssh '' ssh://xonotic@git.xonotic.org/ '' "$@" git '' git://nl.git.xonotic.org/xonotic/ '' "$@" http '' http://nl.git.xonotic.org/xonotic/ '' "$@" git '' git://us.git.xonotic.org/xonotic/ '' "$@" http '' http://us.git.xonotic.org/xonotic/ '' # Gitlab host (divVerent). # Disabled because of https://gitlab.com/gitlab-com/support-forum/issues/15 "$@" http '' https://gitlab.com/xonotic/ '' # German host (divVerent). "$@" git de git://de.git.xonotic.org/xonotic/ '' "$@" http de http://de.git.xonotic.org/xonotic/ '' # Pushing destination (authoritative server; merlijn). "$@" ssh push ssh://git@gitlab.com/xonotic/ '' } 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