diff options
| author | Guillaume Melquiond | 2014-10-24 18:37:10 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2014-10-24 18:37:59 +0200 |
| commit | 9973cd2ca529076388710e90f2c46180581397cf (patch) | |
| tree | a057addf5e8873d5b8804969a62a07e47bbdd66c /plugins | |
| parent | 604621edc81f1c439af5c36ee31c6977c6c3f9f0 (diff) | |
Install index_urls.txt in a location where coqide might actually find it.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions