diff options
| author | Dario Nieuwenhuis <[email protected]> | 2024-01-26 14:23:51 +0100 |
|---|---|---|
| committer | Dario Nieuwenhuis <[email protected]> | 2024-01-26 14:23:51 +0100 |
| commit | adb024bdbe49ba77b3f30af016c0c2ee184f456b (patch) | |
| tree | b0eaaa86ca866a78287340bfdf81a941887dc980 /.github | |
| parent | 73cfa8f8a9b1c462c829b82a534af96cc652bb39 (diff) | |
usb-dfu: add docs metadata.
Diffstat (limited to '.github')
| -rwxr-xr-x | .github/ci/doc.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.github/ci/doc.sh b/.github/ci/doc.sh index d0aff1e43..7112d8aaa 100755 --- a/.github/ci/doc.sh +++ b/.github/ci/doc.sh | |||
| @@ -1,7 +1,7 @@ | |||
| 1 | #!/bin/bash | 1 | #!/bin/bash |
| 2 | ## on push branch=main | 2 | ## on push branch=main |
| 3 | 3 | ||
| 4 | set -euo pipefail | 4 | set -euxo pipefail |
| 5 | 5 | ||
| 6 | export RUSTUP_HOME=/ci/cache/rustup | 6 | export RUSTUP_HOME=/ci/cache/rustup |
| 7 | export CARGO_HOME=/ci/cache/cargo | 7 | export CARGO_HOME=/ci/cache/cargo |