aux.* is a reserved filename in Windows. Rename to auxiliary.
Update the documentation.
Please register or sign in to comment
On Thursday, 7th July from 1 to 3 pm there will be a maintenance with a short downtime of GitLab.
Update the documentation.