Zulip Chat Archive

Stream: general

Topic: history


view this post on Zulip Kenny Lau (Mar 02 2019 at 22:45):

2019-03-02-2.png

view this post on Zulip Kenny Lau (Mar 02 2019 at 22:45):

the picture explains itself (hopefully)

view this post on Zulip Chris Hughes (Mar 02 2019 at 22:47):

Oh dear.

view this post on Zulip Kenny Lau (Mar 02 2019 at 22:47):

@Chris Hughes that's why I edit history

view this post on Zulip Chris Hughes (Mar 02 2019 at 22:48):

I think history is useful to review the PR, but we should squash before merging.

view this post on Zulip Kenny Lau (Mar 02 2019 at 22:49):

yes but if you edited the history then there would be no opportunity to mess up

view this post on Zulip Kenny Lau (Mar 02 2019 at 22:49):

(he apologized under the PR, I noticed just after posting this)

view this post on Zulip Kenny Lau (Mar 02 2019 at 22:50):

how useful is "This year is 2019" anyway for reviewing the PR?

view this post on Zulip Chris Hughes (Mar 02 2019 at 22:51):

Not very. I accidentally put 2018 in the header.

view this post on Zulip Kenny Lau (Mar 02 2019 at 22:51):

I can tell

view this post on Zulip Kenny Lau (Mar 02 2019 at 22:51):

(btw do you know that you can just \copyright)

view this post on Zulip Chris Hughes (Mar 02 2019 at 22:52):

How does that work. It just gives me a copyright symbol.

view this post on Zulip Kenny Lau (Mar 02 2019 at 22:53):

2019-03-02-3.png

view this post on Zulip Kenny Lau (Mar 02 2019 at 22:53):

(the extra options are all the same, don't ask me why)

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Mar 02 2019 at 22:54):

who cares, just replace it manually

view this post on Zulip Scott Morrison (Mar 02 2019 at 23:07):

why not patch it?

view this post on Zulip Kenny Lau (Mar 02 2019 at 23:08):

its in leanprover/mathlib there will be no rebase. only monotone updates

view this post on Zulip Kenny Lau (Mar 02 2019 at 23:08):

-- somebody, a few months ago

view this post on Zulip 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.)

view this post on Zulip Kenny Lau (Mar 02 2019 at 23:10):

well according to somebody, there is to be no rebase in the upstream mathlib

view this post on Zulip Kenny Lau (Mar 02 2019 at 23:10):

i.e. editing the history of leanprover-community/mathlib is forbidden

view this post on Zulip Kenny Lau (Mar 02 2019 at 23:11):

wait

view this post on Zulip Kenny Lau (Mar 02 2019 at 23:11):

what were you referring to

view this post on Zulip Kenny Lau (Mar 02 2019 at 23:11):

the history or the empty set?

view this post on Zulip Scott Morrison (Mar 02 2019 at 23:11):

I was proposing that someone patch the empty set problem :-)

view this post on Zulip Kenny Lau (Mar 02 2019 at 23:11):

I assumed the history because that's the name of this thread

view this post on Zulip Scott Morrison (Mar 02 2019 at 23:11):

Sorry, I see the source of the confusion now!

view this post on Zulip 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