aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorstuebinm2024-04-17 01:55:56 +0200
committerstuebinm2024-04-17 02:01:35 +0200
commit58f5b808c151a801ab5fca2c84a71d3bfddce57d (patch)
treef5e9660be6425f39bce64ca3f5e9e70ebc16193f /tools
parent385e15fc22f48a1f8d40b8263a54155fdab499ea (diff)
general housekeeping
jumps to GHC2021 as default language, adds in some fields, moves the old org mode glossary to markdown, etc.
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions