Closed palmskog closed 2 years ago
Sounds good to me. @maximedenes: what do you think of this change?
How about having a "Source code" item in the main menu, instead of the banner, then?
I guess the "Old news" is less critical, for exemple, isn't it?
@maximedenes I added a menu link, see aaa32e9. "Source Code" doesn't look great, maybe just "GitHub" or "Coq on GitHub" would be better?
@maximedenes any comments here? Do you prefer "Source Code" or "Coq on GitHub" in the menu?
"Source Code" looks fine to me, so I would be inclined to merge as is. But @palmskog let me know if you prefer to change to another link name.
No particular big attachment here, I'm totally fine with "Source Code". So please merge if you think it's good enough.
OK, let's merge then. We can always refine further later.
The "Fork me on GitHub" banner is driving me nuts by covering up many menu links when I browse the Coq website on smaller (narrower) screens, such as mobile phones and tablets. I also feel it is a remnant from the past when GitHub was new and hip, and people went wild forking stuff left and right. Nowadays, the preferred way to start the path to contributing to Coq is probably not by forking it, but discussing on the Zulip, submitting issues, etc.
In this PR, I remove the banner and instead add an explicit reference to GitHub under "Contributing to Coq" on the index page. I also fixed a typo there and changed the wording slightly.