log TOOLS/mencvcd.sh @ 28678:c48f4a1835da

age author description
Mon, 07 Jul 2008 09:32:21 +0000 diego Run bash-specific shell scripts with bash, not sh.
Mon, 07 Jul 2008 09:30:22 +0000 diego Give all shell scripts a .sh suffix for consistency.