diff options
| author |  Jason Gross <jagro@google.com> | 2018-08-03 11:56:28 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-08-04 00:48:46 -0400 |
| commit | ba456dc393f88b281407685896b62f83fd914b7f (patch) | |
| tree | de1191d974ab4e01c2591f7e21e46dec9c82fdca /Makefile | |
| parent | 022b74131203433bd21bf763e5ef8f63c6d678af (diff) | |
Backwards compatible fix for some issues from https://github.com/coq/coq/pull/8200
Diffstat (limited to 'Makefile')
0 files changed, 0 insertions, 0 deletions