diff options
| author | Emilio Jesus Gallego Arias | 2018-05-08 00:52:33 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-05-08 00:52:33 +0200 |
| commit | e9bd8cd805b7b350fe3a970e6be1c9ea2e88a1e8 (patch) | |
| tree | 1fb0a9ac511c8fe2b281f08ed6d915e38efd9a9f /kernel/nativecode.mli | |
| 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 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions