infotheo icon indicating copy to clipboard operation
infotheo copied to clipboard

add redirections to removed items in changedlog.txt

Open t6s opened this issue 3 years ago • 0 comments

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.

t6s avatar Jan 18 '22 11:01 t6s