Re: `master` is now `main`

[Eli Zaretskii]

> From: Stefan Monnier <monnier@iro.umontreal.ca>
> Date: Sat, 19 Dec 2020 00:33:47 -0500
> 
>     git checkout -b main origin/main
> 
> If you have local changes, you'll want to `git stash` before doing that
> and `git stash pop` afterwards and it will likely give you non-trivial
> conflicts to resolve.  Don't hesitate to ask if you need help resolving
> such conflicts.
> 
> Note also that the new branch uses new code, so you'll need to do one
> 
>     make
> 
> as a first step (to fetch the scripts and setup the real makefile) and
> after that it should work more or less as before

Could you please show a list of commands to run manually instead of
that "make" step?  For various boring reasons, I'd prefer not to run
Make in the repository, but instead perform the commands it invokes by
hand.

Thanks.