Thanks for the PR, but unfortunately this contribution will not be accepted as noted in ticket 334:

This is not open to contributors, except for the maintainers. A pull request resolving this is not desired; it would cause a lot of noise on the commit history because of how GitHub handles pull requests.

I do already have in mind how and when this change should be done, and there is no particular rush for it.

Was this PR motivated by struggles with GitHub file formatting (i.e. of Luau features)? If so, we could temporarily change the gitattributes to markup/highlight .lua files as Luau.

Ah I understand.

Was this PR motivated by struggles with GitHub file formatting (i.e. of Luau features)? If so, we could temporarily change the gitattributes to markup/highlight .lua files as Luau.

There were no motivations besides simply noticing files were still using the .lua extension instead of .luau while messing around with various things in the code.

I made the file name changes and noticed an issue was open with a matching description. I didn't notice the remark inside the issue stating that a pull request wasn't desired - my apologies.

I do already have in mind how and when this change should be done, and there is no particular rush for it.

Any more information on this?