tuned GUI;
authorwenzelm
Tue, 13 Jun 2017 11:34:05 +0200
changeset 66079 18e8d4e7ca28
parent 66078 9a719681309e
child 66080 066f4ba9c965
tuned GUI;
src/Tools/VSCode/extension/src/preview.ts
--- a/src/Tools/VSCode/extension/src/preview.ts	Tue Jun 13 11:13:34 2017 +0200
+++ b/src/Tools/VSCode/extension/src/preview.ts	Tue Jun 13 11:34:05 2017 +0200
@@ -91,7 +91,8 @@
 
   if (!active_editor) return ViewColumn.One
   else if (!split) return active_editor.viewColumn
-  else if (active_editor.viewColumn === ViewColumn.One) return ViewColumn.Two
+  else if (active_editor.viewColumn === ViewColumn.One ||
+    active_editor.viewColumn === ViewColumn.Three) return ViewColumn.Two
   else return ViewColumn.Three
 }