diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-01-13 09:16:19 -0800 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-13 09:16:19 -0800 |
| commit | 06b27c26e23a7f783c408535fe40565f3497abf5 (patch) | |
| tree | 073f0cc39cd93f6f5eb65940b884078427ac44fa /ide | |
| parent | 1f63d4f24aab75fab2a3586e194c09a02e5028e2 (diff) | |
| parent | 8de997434f5002728840123dab3aa3e899d1d3f2 (diff) | |
Merge PR #6581: Added newline at the end of usage of coqdep.
Diffstat (limited to 'ide')
0 files changed, 0 insertions, 0 deletions