Hi Qian, when I look at the recent commits, I see something like
Author: Frédéric Chapoton <[email protected]> 2021-01-21 10:59:13 Committer: oldk <[email protected]> 2021-01-22 11:18:10 or Author: Frédéric Chapoton <[email protected]> 2021-01-22 11:11:51 Committer: GitHub <[email protected]> 2021-01-22 11:11:51 Is it possible to use your usual git name and email for the Committer? Or doesn't let github enable us to select the committer? I would know how to set the committer locally, but on github? Doesn't it agree with your credentials? Ralf -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/ca313964-8eff-c177-19f3-2ada8e73d350%40hemmecke.org.
