kre 2eaf0c70b0 Convert from getopt to getopts (script is slightly smaller as a
result, but not enough to save a block ... but if /usr/bin/getopt is
not used elsewhere, and it should not be, it will no longer be required.)
2018-09-22 03:29:51 +00:00
..