From 5f432c0a5c429e0622e4b5801ce21c22a090f81d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Timoth=C3=A9e=20Floure?= <timothee.floure@posteo.net>
Date: Fri, 6 Dec 2019 07:56:28 +0100
Subject: [PATCH] Import missing .vscode configuration folder (dotty-trace
 VSCode plugin)

---
 .vscode/settings.json | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 .vscode/settings.json

diff --git a/.vscode/settings.json b/.vscode/settings.json
new file mode 100644
index 0000000..a35362b
--- /dev/null
+++ b/.vscode/settings.json
@@ -0,0 +1,8 @@
+{
+  "dotty": {
+    "trace": {
+      "remoteTracingUrl": "wss://lamppc36.epfl.ch/dotty-remote-tracer/upload/lsp.log",
+      "server": { "format": "JSON", "verbosity": "verbose" }
+    }
+  }
+}