diff options
| author | Enrico | 2016-01-06 20:46:03 +0100 |
|---|---|---|
| committer | Enrico | 2016-01-06 20:46:03 +0100 |
| commit | c450f3314900aa69f9d456a55d40f7a6adee762b (patch) | |
| tree | 138c376fd4e8af75082d4ab29fd75b07769450cc /etc/ANNOUNCE-github.md | |
| parent | 7780c22d12484785f480057df9f3396a52fb19f5 (diff) | |
| parent | ab782048a148271919ed2e11debff674892f4c95 (diff) | |
Merge pull request #13 from strub/master
do not use `sed -i' in ssrcoqdep -- this is not portable
Diffstat (limited to 'etc/ANNOUNCE-github.md')
0 files changed, 0 insertions, 0 deletions