# HG changeset patch
# User ivo
# Date 1126020612 0
# Node ID 13ac8d0ba7fde5381e88138e3a9da2926a3d1b2a
# Parent  4a1faa9c8f078822cbf2400ede5d4ab6c439ec71
10l

diff -r 4a1faa9c8f07 -r 13ac8d0ba7fd TOOLS/checktree.sh
--- a/TOOLS/checktree.sh	Tue Sep 06 15:15:27 2005 +0000
+++ b/TOOLS/checktree.sh	Tue Sep 06 15:30:12 2005 +0000
@@ -172,7 +172,7 @@
         disable_all_tests
         ;;
     -none)
-        disable_all
+        disable_all_tests
         ;;
     -*)
         echo "unknown option: $i" >&2