diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-08 10:15:31 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-08 10:15:31 +0200 |
| commit | ea2d6b70ed06c60dba9ba81cf53883c85fb92068 (patch) | |
| tree | d0ac3273943f124a59cd3f20aaa007589929a700 /lib/Lattice.v | |
| parent | db2445b3b745abd1a26f5a832a29ca269c725277 (diff) | |
| download | compcert-ea2d6b70ed06c60dba9ba81cf53883c85fb92068.tar.gz compcert-ea2d6b70ed06c60dba9ba81cf53883c85fb92068.zip | |
Added responsefile support for commandline.
Commandline can now be passed in a file specifed with @file on the
Commandline. The quoting convention is similar to the one used by
gcc, etc. Options are separated by whitespaces and options with
whitespaecs need to be quoted.
Bug 18303
Diffstat (limited to 'lib/Lattice.v')
0 files changed, 0 insertions, 0 deletions