Zulip Chat Archive
Stream: general
Topic: history
Kenny Lau (Mar 02 2019 at 22:45):
Kenny Lau (Mar 02 2019 at 22:45):
the picture explains itself (hopefully)
Chris Hughes (Mar 02 2019 at 22:47):
Oh dear.
Kenny Lau (Mar 02 2019 at 22:47):
@Chris Hughes that's why I edit history
Chris Hughes (Mar 02 2019 at 22:48):
I think history is useful to review the PR, but we should squash before merging.
Kenny Lau (Mar 02 2019 at 22:49):
yes but if you edited the history then there would be no opportunity to mess up
Kenny Lau (Mar 02 2019 at 22:49):
(he apologized under the PR, I noticed just after posting this)
Kenny Lau (Mar 02 2019 at 22:50):
how useful is "This year is 2019" anyway for reviewing the PR?
Chris Hughes (Mar 02 2019 at 22:51):
Not very. I accidentally put 2018 in the header.
Kenny Lau (Mar 02 2019 at 22:51):
I can tell
Kenny Lau (Mar 02 2019 at 22:51):
(btw do you know that you can just \copyright)
Chris Hughes (Mar 02 2019 at 22:52):
How does that work. It just gives me a copyright symbol.
Kenny Lau (Mar 02 2019 at 22:53):
Kenny Lau (Mar 02 2019 at 22:53):
(the extra options are all the same, don't ask me why)
Chris Hughes (Mar 02 2019 at 22:54):
That gave me a header, but it started with the empty set instead of a forward slash.
Kenny Lau (Mar 02 2019 at 22:54):
who cares, just replace it manually
Scott Morrison (Mar 02 2019 at 23:07):
why not patch it?
Kenny Lau (Mar 02 2019 at 23:08):
its in leanprover/mathlib there will be no rebase. only monotone updates
Kenny Lau (Mar 02 2019 at 23:08):
-- somebody, a few months ago
Scott Morrison (Mar 02 2019 at 23:10):
Sorry, didn't understand. (I have to admit, Kenny, you're sometimes cryptic to the point it's frustrating.)
Kenny Lau (Mar 02 2019 at 23:10):
well according to somebody, there is to be no rebase in the upstream mathlib
Kenny Lau (Mar 02 2019 at 23:10):
i.e. editing the history of leanprover-community/mathlib is forbidden
Kenny Lau (Mar 02 2019 at 23:11):
wait
Kenny Lau (Mar 02 2019 at 23:11):
what were you referring to
Kenny Lau (Mar 02 2019 at 23:11):
the history or the empty set?
Scott Morrison (Mar 02 2019 at 23:11):
I was proposing that someone patch the empty set problem :-)
Kenny Lau (Mar 02 2019 at 23:11):
I assumed the history because that's the name of this thread
Scott Morrison (Mar 02 2019 at 23:11):
Sorry, I see the source of the confusion now!
Jeremy Avigad (Mar 03 2019 at 14:29):
All, I am sorry I screwed up the merge of Chris'. I am not used to using the Github interface directly, and I thought the "rebase and merge" option would let me edit the commit history. (In other words, I should have used "squash and merge".)
Last updated: Dec 20 2023 at 11:08 UTC