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 /etc/machine.sh | |
parent | 022b74131203433bd21bf763e5ef8f63c6d678af (diff) |
Backwards compatible fix for some issues from https://github.com/coq/coq/pull/8200
Diffstat (limited to 'etc/machine.sh')
0 files changed, 0 insertions, 0 deletions