diff options
author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2015-10-26 09:34:10 -0700 |
---|---|---|
committer | Bernhard Schommer <bschommer@users.noreply.github.com> | 2015-10-26 09:34:10 -0700 |
commit | dcee0b9232aeb05bf7fdf57718c00656a28af2f8 (patch) | |
tree | 0c11fbdedba33fd3d3249c69d0278aaf6b0c95d9 /.gitignore | |
parent | 22ba27a76497ac06fdaddf5a54346107a4727f6f (diff) | |
parent | c1492881a211b30bf4e18732da1744eeae13a445 (diff) | |
download | compcert-dcee0b9232aeb05bf7fdf57718c00656a28af2f8.tar.gz compcert-dcee0b9232aeb05bf7fdf57718c00656a28af2f8.zip |
Merge pull request #61 from fpottier/clean
Fixed one error message and removed two comments.
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions