Fri, 30 Dec 2016 10:26:10 +0100 | wenzelm | tuned; | file | diff | annotate |
Thu, 29 Dec 2016 22:10:29 +0100 | wenzelm | re-use options from resources; | file | diff | annotate |
Thu, 29 Dec 2016 21:54:04 +0100 | wenzelm | moved main state to VSCode_Resources; | file | diff | annotate |
Wed, 21 Dec 2016 11:41:05 +0100 | wenzelm | clarified node_name: preserve original uri; | file | diff | annotate |
Tue, 20 Dec 2016 22:32:04 +0100 | wenzelm | clarified module name; | file | diff | annotate | base |