src/Tools/VSCode/etc/options

--- a/src/Tools/VSCode/etc/options	Tue Jan 10 17:24:15 2017 +0100
+++ b/src/Tools/VSCode/etc/options	Wed Jan 11 14:22:57 2017 +0100
@@ -17,3 +17,6 @@
 
 option vscode_timing_threshold : real = 0.1
   -- "default threshold for timing display (seconds)"
+
+option vscode_unicode_symbols : bool = false
+  -- "output Isabelle symbols via Unicode (according to etc/symbols)"