+ [2020-01-15T19:41:22Z] cousteau wonders why didn't they name the files .coq ... then again Verilog hadn't been around that long when Coq was invented, and probably nobody expected a case where both would be used simultaneously
+ [2020-01-15T19:46:26Z] cousteau https://github.com/cliffordwolf/picorv32/search?l=verilog&p=4 Now THIS is weird. See picorv32.v in that list? Well, that's the file being erroneously identified as Coq when you open it in github
+ [2020-01-15T22:57:56Z] jaakkos Is there a supported way to change TLS certificate for GitHub Enterprise Server over SSH or some other non-interactive manner that can be automated? (Let's Encrypt is not an option)
+ [2020-01-15T23:07:15Z] jaakkos The answer seems to be ghe-config.
+ [2020-01-15T23:07:24Z] jaakkos (+ ghe-config-apply)

message no. 176423

Posted by cousteau in #github at 2020-01-15T19:23:14Z

Hi! How does Github know how to highlight files? It seems to have incorrectly detected a Verilog file as Coq (both use .v extensions)
+ [2020-01-16T17:39:05Z] causasui can I add a group to CODEOWNERS and expect similar behavior as if a user were added?
+ [2020-01-16T17:39:22Z] causasui docs seem to be silent on this
+ [2020-01-16T22:36:03Z] Seveas causasui: yes, grous can be in CODEOWNERS, we use this a lot
+ [2020-01-17T02:22:32Z] mrproper I am running a Github training and can't assume everyone has a Github account. Because generating SSH keys during class will taunt the demo gods, I'd like to have them use HTTPS for the sake of the lab. I am trying it out and set my origin URL to `https://user:pass@github.com/...` but it's giving me an invalid username and password. Am I doing something wrong? If not, I have 2FA enabled and wonder if that's a problem.
+ [2020-01-17T02:30:18Z] mrproper It needs a token. Thanks.