diff options
| author | Enrico Tassi | 2021-01-06 14:19:59 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2021-01-27 09:45:49 +0100 |
| commit | 4c4d6cfacf92b555546055a45edc19b68245b83c (patch) | |
| tree | 3229ea96990a91d015e8059f678f67a431a1cf3b /sysinit/usage.ml | |
| parent | 4264aec518d5407f345c58e18e014e15e9ae96af (diff) | |
[sysinit] move initialization code from coqtop to here
We also spill (some) non-generic arguments and initialization code
out of coqargs and to coqtop, namely colors for the terminal. There are
more of these, left to later commits.
Diffstat (limited to 'sysinit/usage.ml')
0 files changed, 0 insertions, 0 deletions