Yeah, you’re right, I too would prefer Ctrl+F to work as usual. In hindsight I guess I came across a bit strong, but I had been leafing through the jargon file (it’s history for nerds; awesome history) and couldn’t help but shove that wart comment in there. 
1 Like