When running `sudo make install`, we only want to run the actual install as root, the building of the documentation and the distribution folder should happen as the non-root user. Related to #13728.
make TAGS.vi
sudo make install