Remove the comma in the committer name ("Dzomo, the Everest Yak")

project-everest / everest-ci

CI scripts for project everest

3 stars 8 forks source link

Remove the comma in the committer name ("Dzomo, the Everest Yak") #37

Closed msprotz closed 7 years ago

msprotz commented 7 years ago

This causes conflicts with the email gateway for email notifications and is causing Catalin some trouble.

Task description:

to be performed in the Linux and Windows environments
edit the ~/.gitconfig file
change the name key in the [user] section to just remove the comma
in case of trouble, this is the documentation for git config https://git-scm.com/docs/git-config

CC @catalin-hritcu

darrenge commented 7 years ago

I went in and fixed this. I see for new docker container has it fixed already and I updated the existing agents (FStar and FStar2). I also updated the Windows .gitconfig as well.

catalin-hritcu commented 7 years ago

@darrenge Seems to work, many thanks.