Open kohlhase opened 5 years ago
it would be nice if the great new view source button could be extended by an edit source button, which which links to the web IDE of GitLab, e.g. https://gl.mathhub.info/-/ide/project/MitM/smglom/edit/master/-/source/graphs/graphs.mmt Maybe changing to
source: <button>view</button> <button>edit</button>
or something like this
it would be nice if the great new view source button could be extended by an edit source button, which which links to the web IDE of GitLab, e.g. https://gl.mathhub.info/-/ide/project/MitM/smglom/edit/master/-/source/graphs/graphs.mmt Maybe changing to
or something like this