# HG changeset patch
# User wenzelm
# Date 1014283500 -3600
# Node ID 0e144958cf279ef4d1a7ee4e8860abefc91fe655
# Parent  704713ca07eada8af4431d230aa9ea3f7d8f06f6
tr: quote argument;

diff -r 704713ca07ea -r 0e144958cf27 lib/Tools/usedir
--- a/lib/Tools/usedir	Thu Feb 21 09:54:08 2002 +0100
+++ b/lib/Tools/usedir	Thu Feb 21 10:25:00 2002 +0100
@@ -51,7 +51,7 @@
 
 function check_number()
 {
-  [ -n "$1" -a -z "$(echo "$1" | tr -d [0-9])" ] || fail "Bad number: \"$1\""
+  [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
 }