Commit d4c80b4
authored
Delete duplicated docs folders (#3780)
# Description of Changes
Somehow (apparently after #3494) we wound up with a bunch of duplicate
folders in our repo, both the old title-case names and the new
lower-case names. All of the remaining files in the title-case
directories have their last change in #3343, well before #3494, so I
don't believe we're losing any intermediate changes by deleting them.
I'm not sure how this happened, but it seems to be an easy fix.
# API and ABI breaking changes
N/a
# Expected complexity level and risk
2 - some small possibility that I accidentally deleted an intentional
change that got borked by a merge conflict or something. I don't think I
did, tho, based on the age of the git blame on the files deleted here.
# Testing
None1 parent 9c6e5a5 commit d4c80b4
File tree
10 files changed
+0
-1722
lines changed- docs/docs
- 08-SQL
- 09-Subscriptions
- 12-SpacetimeAuth
- 14-Internals
- 15-Appendix
10 files changed
+0
-1722
lines changedThis file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
0 commit comments