search

leanprover / vscode-lean4

Visual Studio Code extension for the Lean 4 proof assistant
Apache License 2.0
158 stars 48 forks source link

Initial commit does not work in fresh install of Git #510

Closed mhuisi closed 2 months ago

mhuisi commented 2 months ago

Output:

> git commit --author "Lean 4 VS Code Extension <>" -m "Initial commit"
Committer identity unknown

*** Please tell me who you are.

Run

  git config --global user.email "you@example.com"
  git config --global user.name "Your Name"

to set your account's default identity.
Omit --global to set the identity only in this repository.

fatal: unable to auto-detect email address (got '[...]')

=> Operation failed. Exit code: 128.