[Merged by Bors] - fix: update scripts/rm_set_option.py to ignore more comments - #41997

[Merged by Bors] - fix: update scripts/rm_set_option.py to ignore more comments#41997

vlad902 wants to merge 2 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

vlad902:fix-rm-setoptionvlad902/mathlib4:fix-rm-setoptionCopy head branch name to clipboard