[workspace-hack] use workspace-dotted format and a patch directive#986

Merged

sunshowers merged 2 commits intomainfrom sunshowers/spr/workspace-hack-use-workspace-dotted-format-and-a-patch-directive

Oct 4, 2023

+110-105

Commits on Oct 4, 2023