David Tolnay 1ee932f7a2 Destroy history of github-pages branch (#3783) ... ## Motivation and Context Keeping the history of `github-pages` is not useful, and it hogs the output of `git log --graph --all` and other such views of the repository history. In the event that someone would need to look at old contents of the website, it can be regenerated using `mdbook` from any commit on `main`. <img src="https://github.com/user-attachments/assets/f37630fa-92ef-4e49-a9e5-a1357a785e46" width="550"> ---- _By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice._		2024-08-07 02:49:18 +00:00
..
ISSUE_TEMPLATE	Fix repeated options when creating an issue (#1916)	2022-10-28 10:12:19 +01:00
actions	Allow artifacts of the same name to be overwritten (#3509)	2024-03-25 18:28:19 +00:00
scripts	Remove flags from release (#3521)	2024-03-29 14:30:38 +00:00
workflows	Destroy history of github-pages branch (#3783)	2024-08-07 02:49:18 +00:00
PULL_REQUEST_TEMPLATE.md	Switch to file-per-change changelog (#3774)	2024-08-01 04:31:19 +00:00