infotheo
infotheo copied to clipboard
add redirections to removed items in changedlog.txt
changelog.txt
currently lists removed Definitions / Lemmas / etc. but not what to use instead, making the user stuck at upgrading their scripts dependent on the removed things.
This draft PR is an attempt to add comments to previously removed items. I am not sure how thoroughly this should be done, thus just a draft.