--- a/lib/Tools/mkdir Tue Jul 04 01:10:36 2000 +0200
+++ b/lib/Tools/mkdir Tue Jul 04 01:10:53 2000 +0200
@@ -12,7 +12,7 @@
function usage()
{
echo
- echo "Usage: $PRG [LOGIC] NAME"
+ echo "Usage: $PRG [OPTIONS] [LOGIC] NAME"
echo
echo " Options are:"
echo " -I FILE alternative IsaMakefile output"