Is it possible to change the name of the restAPI.jar plugin? I would like to name it restAPI-1.2.5.jar. The docs seem to indicate, implicitly, that it should be fine. Even if file name does not matter to the plugin system, it might matter to the plugin itself.