diff options
| author | Hugo Herbelin | 2019-04-27 22:21:49 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-04-27 22:21:52 +0200 |
| commit | b1a22c6e7584dce2a8294cb29ddada39173ced8a (patch) | |
| tree | a1d74a9772445065a119b2ad4f72c9fe306a96ca /dev | |
| parent | 9b2cbdcdaac203999484ef90225f6cba5e8052db (diff) | |
CoqIDE, cosmetic: removing obsolete comments.
There is no more uses of "old style preferences" but the comment was
still there.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions