From 846ed09c07ea1022b5f163bb48beea0cf062fc4e Mon Sep 17 00:00:00 2001 From: Kreyren Date: Tue, 18 Feb 2020 11:39:07 +0000 Subject: [PATCH] Finally we have theia config Relevant: https://github.com/gitpod-io/gitpod/issues/800#issuecomment-587381366 --- .theia/README.md | 3 +++ {workspace/Zernif/.vscode => .theia}/settings.json | 0 workspace/README.md | 3 --- 3 files changed, 3 insertions(+), 3 deletions(-) create mode 100644 .theia/README.md rename {workspace/Zernif/.vscode => .theia}/settings.json (100%) delete mode 100644 workspace/README.md diff --git a/.theia/README.md b/.theia/README.md new file mode 100644 index 0000000..3361ffd --- /dev/null +++ b/.theia/README.md @@ -0,0 +1,3 @@ +Configuration directory for [theia](https://github.com/eclipse-theia/theia) + +Theia is also used by gitpod \ No newline at end of file diff --git a/workspace/Zernif/.vscode/settings.json b/.theia/settings.json similarity index 100% rename from workspace/Zernif/.vscode/settings.json rename to .theia/settings.json diff --git a/workspace/README.md b/workspace/README.md deleted file mode 100644 index e098bbf..0000000 --- a/workspace/README.md +++ /dev/null @@ -1,3 +0,0 @@ -Annoying directory that is recognized by Theia (GitPod) to export our configuration - -FIXME: Make theia to recognize `gitpod` and NUKE this abomination from my repo \ No newline at end of file