diff options
| author | Pierre-Yves Strub | 2016-01-05 22:17:24 -0800 |
|---|---|---|
| committer | Pierre-Yves Strub | 2016-01-05 22:19:48 -0800 |
| commit | ab782048a148271919ed2e11debff674892f4c95 (patch) | |
| tree | 138c376fd4e8af75082d4ab29fd75b07769450cc /etc/ANNOUNCE-github.md | |
| parent | 7780c22d12484785f480057df9f3396a52fb19f5 (diff) | |
do not use `sed -i' in ssrcoqdep -- this is not portable
This prevents compilation of ssreflect on OS-X/*BSD.
Diffstat (limited to 'etc/ANNOUNCE-github.md')
0 files changed, 0 insertions, 0 deletions