diff options
| author | Hugo Herbelin | 2020-04-17 20:19:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-19 14:42:23 +0200 |
| commit | cf97da30c680cc45113742e6744ed34fb87ab9f2 (patch) | |
| tree | 07345ee37953b3267c41b970bc65014ae5afec68 /dev/ci | |
| parent | ae1f5246e192f2b75fcdd1d454e306614ab7efb3 (diff) | |
CoqIDE: Adding a short documentation on style/theme customization.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions