Skip to content

Map editing tools and improved local mapping #93

Map editing tools and improved local mapping

Map editing tools and improved local mapping #93

Triggered via pull request December 12, 2024 16:34
Status Success
Total duration 5m 55s
Artifacts 2

docs.yml

on: pull_request
Draft Release
0s
Draft Release
Publish to GH Pages
0s
Publish to GH Pages
Fit to window
Zoom out
Zoom in

Artifacts

Produced during runtime
Name Size Digest
documentation-pdf Expired
491 KB
sha256:7768035288864f2e9bd5ca25985da029782063102e4337d8a055a0ce46a6d847
github-pages Expired
6.97 MB
sha256:c418c9a555d8df1f8084df84489664259624176fddbcda84bac0ebce090dce97