[Documentation:Developer] Add new lint scripts to docs#671

bmcutler merged 1 commit intomainSubmitty/submitty.github.io:mainfrom

add-new-lint-scripts-to-docsSubmitty/submitty.github.io:add-new-lint-scripts-to-docsCopy head branch name to clipboard