Add option to set default file extension and disable rich editing#2718
Merged
juliusknorr merged 1 commit intomasterfrom Jul 19, 2022
Merged
Add option to set default file extension and disable rich editing#2718juliusknorr merged 1 commit intomasterfrom
juliusknorr merged 1 commit intomasterfrom
Commits
Commits on Jul 19, 2022
- authored andcommitted
