Michael 0a3b20d8b2 Replace deprecated linting and formatting settings by extensions (#104050)		2023-11-16 23:10:33 +01:00
..
devcontainer.json	Replace deprecated linting and formatting settings by extensions (#104050)	2023-11-16 23:10:33 +01:00