Allright then, I ordered a couple from Mouser, since they weren't expensive. I'll follow up with the repair since I started a thread. Technically, the new switch is a tiny bit higher, in terms of the center of the push rod to the top of the circuit board, by 1.5 mm, but I've checked and that won't make enough difference to matter; i.e. the pushrod will still function OK. All the other dimensions seem to check out OK.

