Commit Graph

2 Commits

Author SHA1 Message Date
kobewi 889f5e44ef Make tool menu plugins use Callables for callback 2020-12-16 20:23:51 +01:00
Fabio Alessandrelli c54de7f589 [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).
2020-10-14 12:31:20 +02:00