diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2020-07-07 18:36:31 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2020-07-08 11:58:11 +0200 |
| commit | 1a01ad629109cdb60fddae3787e3a589d20e9790 (patch) | |
| tree | 02b0b37b65e12373b996bd109309d17b31408b44 /Makefile | |
| parent | ae7eeb880d35fb12b4620e5320a8f9677a72d159 (diff) | |
| download | compcert-1a01ad629109cdb60fddae3787e3a589d20e9790.tar.gz compcert-1a01ad629109cdb60fddae3787e3a589d20e9790.zip | |
Use the same version string.
The version string dumped in the file should be the same as the version
string printed by `-version`. The option is also not printed by `-help`
since it is for internal use only.
Diffstat (limited to 'Makefile')
0 files changed, 0 insertions, 0 deletions