diff options
| author | Fabio Alessandrelli <fabio.alessandrelli@gmail.com> | 2020-09-17 18:01:36 +0200 |
|---|---|---|
| committer | Fabio Alessandrelli <fabio.alessandrelli@gmail.com> | 2020-10-14 12:31:20 +0200 |
| commit | c54de7f5899f2bd64caee65efe16975a179aa51f (patch) | |
| tree | 0b3698d1f16c85151c646e6de496338db930790d /editor/plugins | |
| parent | 3dfb7691152c5bd6bce1b3e550d3978854d83ac7 (diff) | |
[HTML5] Add JavaScriptToolsEditorPlugin.
A new editor plugin, specific to HTML5, that provide some extra features
needed to make the editor usable on that platform.
For now, it adds a "Download project sources" option in the "Tool" menu,
so the user can download the work done as a zip file (from the browser
storage).
Diffstat (limited to 'editor/plugins')
0 files changed, 0 insertions, 0 deletions