Treat - just as /dev/stdin and remove one extra file reader (#1065)
authorEbrahim Byagowi <ebrahim@gnu.org>
Sun, 24 Jun 2018 18:39:16 +0000 (23:09 +0430)
committerGitHub <noreply@github.com>
Sun, 24 Jun 2018 18:39:16 +0000 (23:09 +0430)
commit159ddb872986f121818e816d2ea75d271075ba1f
tree26c363e55756b50d6e9c06b764a748ee9db0dd3d
parentb2a187918757a0faaf0f564ec2b0766c09fa364c
Treat - just as /dev/stdin and remove one extra file reader (#1065)
util/options.cc