Setting up project through GitHub.

Stream: new members

[John Smith]

Hi there! Im pretty new to this so apologises if this is basic, but ive just installed Lean through VSCode and when I created a new project there was a read me with instructions for how to set up a GitHub repo,

## GitHub configuration

To set up your new GitHub repository, follow these steps:

* Under your repository name, click **Settings**.
* In the **Actions** section of the sidebar, click "General".
* Check the box **Allow GitHub Actions to create and approve pull requests**.
* Click the **Pages** section of the settings sidebar.
* In the **Source** dropdown menu, select "GitHub Actions".

After following the steps above, you can remove this section from the README file.

and im just wondering what the point of this is? Can I just ignore this and use GitHub like normal? My concerns are that a) I have no clue what this does and b) it means I need to have my repo public as I don't have a GitHub subscription so I can't use pages with a private repo.

Thanks!

[Kenny Lau]

i don't think this is necessary

[Eric Wieser]

The point of steps 1-3 is to allow the lean-upgrade action to run

[Eric Wieser]

I don't see what the relevance of "pages" is here

[John Smith]

So if I just want a simple project on GitHub, which of these files in the new project do I even need? How much of it is for the automatic updates?