[Autorevert] gitignore /*.html in the main autorevert as a convenience#7520

jeanschmidt wants to merge 2 commits intomainpytorch/test-infra:mainfrom

jeanschmidt/autorevert_ignore_htmlpytorch/test-infra:jeanschmidt/autorevert_ignore_htmlCopy head branch name to clipboard