build warning

Stream: new members

[Michael Beeson]

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?

[Alex Peattie]

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: