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 /.github | |
| 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 '.github')
| -rw-r--r-- | .github/CODEOWNERS | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index fe7913a3d2..56f48aaa4f 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -228,6 +228,7 @@ /toplevel/ @coq/toplevel-maintainers /topbin/ @coq/toplevel-maintainers +/sysinit/ @coq/toplevel-maintainers ########## Vernacular ########## |