diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2016-02-02 09:34:36 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2016-02-02 09:34:36 +0100 |
| commit | 0d6a1557ae45b8c731c6715bb7109a30c32c5a26 (patch) | |
| tree | 1efd61ed8213afeab7992032aef7ed4fccb9461d /driver/Timing.ml | |
| parent | 15fc340f69e9c4d718c15fd9ec12a81695cf8d67 (diff) | |
| parent | 659a1b55f454fc262826e4edf7d938f01ae04263 (diff) | |
| download | compcert-0d6a1557ae45b8c731c6715bb7109a30c32c5a26.tar.gz compcert-0d6a1557ae45b8c731c6715bb7109a30c32c5a26.zip | |
Merge pull request #85 from AbsInt/option_json
Flag -doptions to save machine configuration and command-line flags to a JSON file.
Diffstat (limited to 'driver/Timing.ml')
0 files changed, 0 insertions, 0 deletions