Removed Options sub-menu from Tools menu. I haven't used Options in 15 years.
Authored by: fourshades 2023-05-23
Parent: [r734]
Child: [r736]
