diff options
| author | Joris | 2021-05-20 16:55:01 +0200 |
|---|---|---|
| committer | Joris | 2021-05-20 16:55:01 +0200 |
| commit | 56de4dc516975b36d1cbe70da3964d254fa82c65 (patch) | |
| tree | 73e0eeae0fe4a164cb82d9def9be9ada828bfe8f /src/Model/config.ml | |
| parent | 82e688161e2975696edf43bd9a3a78f39d7d55d0 (diff) | |
Reduce number input widths
Diffstat (limited to 'src/Model/config.ml')
0 files changed, 0 insertions, 0 deletions