rename table "abtleitung"
The table for Abteilungs-Leitung is currently named abtleitung
. That is too easily misread as abteilung
, the name of another table.
So it'd probably be good to rename that table.
Options that come to mind:
abteilungsleitung
abteilung_leitung
abt_leitung
If we rename it, we should review all exercises and sample solutions to see which ones need to be adapted accordingly.