diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-08 00:52:33 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-08 00:52:33 +0200 |
commit | e9bd8cd805b7b350fe3a970e6be1c9ea2e88a1e8 (patch) | |
tree | 1fb0a9ac511c8fe2b281f08ed6d915e38efd9a9f /toplevel/coqtop_opt_bin.ml | |
parent | 6c8b00e47334f60f200256d45a5542fa80ce4b12 (diff) |
[toplevel] Don't ignore output filename provided by user in -o
This was a silly bug introduced in
675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54 that forgot to properly
forward the command line option.
Thanks to @SkySkimmer for finding out the problem.
closes #7447
Diffstat (limited to 'toplevel/coqtop_opt_bin.ml')
0 files changed, 0 insertions, 0 deletions