diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-05-13 17:57:06 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-06-05 22:09:40 -0400 |
| commit | 739ead8b2d70f978e31f793234d7a633636742a1 (patch) | |
| tree | 15da3b48ea04a45333dbe6484f4f47badb912d35 /CREDITS | |
| parent | 51b32595081d279624c8ec162f9ed686ed660d9b (diff) | |
-profileltac -> -profile-ltac, as per @herbelin
https://github.com/coq/coq/pull/150#issuecomment-219141596
```bash
git grep --name-only profileltac | xargs sed s'/profileltac/profile-ltac/g' -i
```
Diffstat (limited to 'CREDITS')
0 files changed, 0 insertions, 0 deletions