diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-04-27 15:40:48 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-09-10 15:02:18 +0200 |
| commit | 238725dd24d43574690b0111761b705753d3bee2 (patch) | |
| tree | 060fb1cdbd5c4ba299459fe50493baeba2a292d4 /ide/preferences.ml | |
| parent | 3140d22d75ac3f30e97c799a05819b8838d167ca (diff) | |
typo in refman.
Diffstat (limited to 'ide/preferences.ml')
0 files changed, 0 insertions, 0 deletions