lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

Git conflict experiment

Open kmill opened this issue 1 year ago • 1 comments

This is an experiment to have git conflict syntax be processed like comments.

The option parser.git.useIncoming controls whether to use the incoming or current versions.

@jcommelin @adomani

kmill avatar Sep 27 '24 19:09 kmill

Mathlib CI status (docs):

  • ✅ Mathlib branch lean-pr-testing-5500 has successfully built against this PR. (2024-09-27 20:50:29) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e3811fd838e0b38edcfad0d52652894fb0e8a017 --onto 5e8718dff9d7906e1d4ca7020256dae7c05e49c2. (2024-10-02 04:04:49)

leanprover-community-bot avatar Sep 27 '24 20:09 leanprover-community-bot