Stream: general

Topic: history

2019-03-02-2.png

Kenny Lau (Mar 02 2019 at 22:45):

the picture explains itself (hopefully)

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.

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.

2019-03-02-3.png

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

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: May 09 2021 at 20:11 UTC