| ▲ | bigstrat2003 12 days ago | |||||||||||||||||||||||||||||||
Yeah, because people are overly sensitive and can't bear the thought that someone might make some harmless naughty jokes. It's a completely ridiculous name change.  | ||||||||||||||||||||||||||||||||
| ▲ | ironmagma 12 days ago | parent | next [-] | |||||||||||||||||||||||||||||||
No. Conversions about it were being avoided due to being in a work context and in general. The same goes for coc (vim plugin) by the way.  | ||||||||||||||||||||||||||||||||
  | ||||||||||||||||||||||||||||||||
| ▲ | nickpsecurity 12 days ago | parent | prev [-] | |||||||||||||||||||||||||||||||
One of my coworkers uses Siri to say what they want to search for. I'm definitely not saying: "Hey, Siri, show me examples of using Coq." Then, users of search engines will add "training," "in the workplace," "visual guide," "positions," "freelance work with," etc. Everything people use with programming languages or book titles becomes inappropriate with that name. Maybe if I worked on a chicken farm it would be OK. I'm in the hotel and retail industries doing a mix of hands-on work and customer service. You'll never hear me tell my bosses I was using that on the job. Or spending hours alone with Isabelle for that matter. HOL4 & HOL Light it is!  | ||||||||||||||||||||||||||||||||
  | ||||||||||||||||||||||||||||||||