Closed Zimmi48 closed 2 years ago
People's names are in two different fonts, how about fixing that? Eg: The boldface on this one seems inconsistent with the other entries: Also, more trivially, "Coq-community manager" is capitalized differently for @Zimmi48 and @palmskog
People's names are in two different fonts, how about fixing that? Eg:
The boldface on this one seems inconsistent with the other entries:
Also, more trivially, "Coq-community manager" is capitalized differently for @Zimmi48 and @palmskog
Originally posted by @jfehrle in https://github.com/coq/www/issues/172#issuecomment-872705392
Note that the different fonts correspond to people whose name links to a website or not.
Originally posted by @jfehrle in https://github.com/coq/www/issues/172#issuecomment-872705392
Note that the different fonts correspond to people whose name links to a website or not.