aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
authorLasse Blaauwbroek2020-12-22 06:15:28 +0100
committerLasse Blaauwbroek2020-12-27 18:26:01 +0100
commitd1af000c4b9b1d1ff9b2f9fbf2dcb570ae7c974c (patch)
tree6ee84b6104fdfacab5a63661b8577a079cc72a3e /dev/ci
parenta84ff9806f0ee77e081954453ee6afb67921eb50 (diff)
Make ssrtermkind algebraic instead of a char
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions