Zulip Chat Archive

Stream: new members

Topic: build warning

view this post on Zulip Michael Beeson (Sep 14 2020 at 19:36):

Every time I do "leanproject build" I get this message:

HEAD is now at c3a6a6990 doc(group_theory/subgroup): fix links in module doc (#4115)

The build seems to work OK. Is there something I can or should do about this message?

view this post on Zulip Alex Peattie (Sep 14 2020 at 19:40):

I don't think that's a warning, it's more of just an info message. HEAD in git is the pointer to your current working revision, so leanproject is just confirming which revision is checked out. You can safely ignore the message :smile:

Last updated: May 16 2021 at 05:21 UTC