lib/Tools/mkdir
changeset 9237 161fb7f00414
parent 8685 05b6e5bcab66
child 9656 a3d868043c49
     1.1 --- a/lib/Tools/mkdir	Tue Jul 04 01:10:36 2000 +0200
     1.2 +++ b/lib/Tools/mkdir	Tue Jul 04 01:10:53 2000 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  function usage()
     1.5  {
     1.6    echo
     1.7 -  echo "Usage: $PRG [LOGIC] NAME"
     1.8 +  echo "Usage: $PRG [OPTIONS] [LOGIC] NAME"
     1.9    echo
    1.10    echo "  Options are:"
    1.11    echo "    -I FILE      alternative IsaMakefile output"