From f0243297b152d2d7d505b0ecbf2001f8e5c8225e Mon Sep 17 00:00:00 2001 From: Renato Alves Date: Wed, 17 Mar 2021 20:30:01 +0100 Subject: [PATCH] Document .editorconfig as alternative to settings.json closes [gitpod-io/gitpod#896] --- src/docs/config-editor.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/docs/config-editor.md b/src/docs/config-editor.md index 7a0b19445..e629de566 100644 --- a/src/docs/config-editor.md +++ b/src/docs/config-editor.md @@ -4,12 +4,15 @@ Gitpod uses [Theia](https://github.com/eclipse-theia/theia) as its IDE which can Workspace settings are stored in a file within your project. They can reside either in: - `$GITPOD_REPO_ROOT/.theia/settings.json` or - - `$GITPOD_REPO_ROOT/.vscode/settings.json` + - `$GITPOD_REPO_ROOT/.vscode/settings.json` or + - `$GITPOD_REPO_ROOT/.editorconfig` User settings override workspace settings and can be configured through the preferences editor, which you can open through the menu (`File -> Preferences`). The available properties and their possible values are proposed in the editor and are the same as in VS Code. +Additionally you can keep settings in [`editorconfig` format](https://editorconfig.org) that takes precedence over other settings. +

Example Configuration

File `settings.json` follows JSON syntax as follows: