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 /.gitignore | |
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 '.gitignore')
0 files changed, 0 insertions, 0 deletions