diff options
| author | Jim Fehrle | 2019-12-02 16:02:31 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2019-12-02 16:02:31 -0800 |
| commit | dd413df1cc2fe27d89e2ef926200e53b50105dda (patch) | |
| tree | b1c5bbe047c1226296777f9a6a5d82e0ed51109e /dev | |
| parent | 79bbca336a226693770e37db3a8f05b2819acb5c (diff) | |
Remove latex files that should be regenerated by make
If these files are present in the latex directory, "make refman-pdf"
may fail to generate CoqRefMan.pdf.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions