+# avoid running several instances of this script
+# when the svn server has problems, this can very well last quite a while
+
+COMMAND=$(basename $0)
+
+# make the command usable as non-root user at Princeton for more efficiency
+if [ "$(id -u)" == "0" ] ; then
+ OUTPUT=/build/modules
+ LOCK=/var/run/all-modules.pid
+else
+ OUTPUT=~/all-modules
+ LOCK=~/all-modules.run
+fi
+
+function do_update() {
+ build_dir=$1; shift
+ if [ -f $build_dir/auto-update.sh ] ; then
+ $build_dir/auto-update.sh
+ else
+ ( cd $build_dir; svn update > .update.log 2>&1 )
+ fi
+}