diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-23 17:38:54 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-23 17:38:54 +0200 |
| commit | 94163429293cef7410320f79fc5964fc546fccef (patch) | |
| tree | 085714716026db33b4f99e7f75595c6b22233c8a /cparser/GNUmakefile | |
| parent | 1cb3d93ff278ebbd0c6967c5f9401a97f9b618b4 (diff) | |
| download | compcert-94163429293cef7410320f79fc5964fc546fccef.tar.gz compcert-94163429293cef7410320f79fc5964fc546fccef.zip | |
Added additional option for the renaming of the suffix of the sdump
file.
The new option -sdump-suffix allows it to specify another suffix
for the sdump file.
Bug 17326
Diffstat (limited to 'cparser/GNUmakefile')
0 files changed, 0 insertions, 0 deletions