diff options
author | Michael Schmidt <github@mschmidt.me> | 2016-06-28 14:25:50 +0200 |
---|---|---|
committer | Michael Schmidt <github@mschmidt.me> | 2016-06-28 14:35:20 +0200 |
commit | 56a6795d82c5ff0af78872a3e807b48c556ce5fe (patch) | |
tree | 8c945b05c650afd7e8aaee077bdf3292fec719e7 /driver/Optionsprinter.ml | |
parent | 5ceb5de6616178217a589874b26d2046b6cc8c5b (diff) | |
download | compcert-56a6795d82c5ff0af78872a3e807b48c556ce5fe.tar.gz compcert-56a6795d82c5ff0af78872a3e807b48c556ce5fe.zip |
bug 19234, inherit varargs flag from previous function definitions for KR conversion
Diffstat (limited to 'driver/Optionsprinter.ml')
0 files changed, 0 insertions, 0 deletions