Skip to content

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

Closed
vlad902 wants to merge 2 commits into
leanprover-community:masterfrom
vlad902:fix-rm-setoption
Closed

[Merged by Bors] - fix: update scripts/rm_set_option.py to ignore more comments#41997
vlad902 wants to merge 2 commits into
leanprover-community:masterfrom
vlad902:fix-rm-setoption