Skip to content

split out a task for running dune exec and add env param in p_run #74

split out a task for running dune exec and add env param in p_run

split out a task for running dune exec and add env param in p_run #74

Triggered via push October 15, 2023 03:43
Status Success
Total duration 7m 54s
Artifacts

odoc.yml

on: push
Fit to window
Zoom out
Zoom in

Annotations

1 notice
deploy-doc
An error has been caught in some system package index files, so the system package index files have been re-synchronised, and the system package installation has been retried: the process '/usr/bin/sudo' failed with exit code 100