.bashrc: Move *_proxy earlier; I do not remember why.

[nethome.git] / bin / errs2

diff --git a/bin/errs2 b/bin/errs2
index cd0da81..17548cb 100755 (executable)
--- a/bin/errs2
+++ b/bin/errs2
@@ -1,5 +1,4 @@
-#! /bin/sh
-# $Id$
+#! /bin/bash
 
 renice +19 -p $$; ionice -c3 -p $$
 
@@ -22,6 +21,9 @@ rm -f $out.ok
 (
        set -ex
        time nice make $j "$@"
+       if [ -d gdb/testsuite ];then
+               make -C gdb/testsuite site.exp
+       fi
        touch $out.ok
        ) 2>&1|tee $args $out
 test -f $out.ok