Bruno Haible
2017-09-08 21:50:18 UTC
gnulib-tool.py --help
shows that a --dir option should be accepted, but it is not.
$ ./gnulib-tool.py --dir=../testdir-dirent --create-testdir dirent
usage: gnulib-tool.py --help
./gnulib-tool.py: error: unrecognized arguments: --dir=../testdir-dirent
Here's the proposed fix. OK to push?
shows that a --dir option should be accepted, but it is not.
$ ./gnulib-tool.py --dir=../testdir-dirent --create-testdir dirent
usage: gnulib-tool.py --help
./gnulib-tool.py: error: unrecognized arguments: --dir=../testdir-dirent
Here's the proposed fix. OK to push?