diff options
| author | Dario Nieuwenhuis <[email protected]> | 2023-05-31 12:31:28 +0000 |
|---|---|---|
| committer | GitHub <[email protected]> | 2023-05-31 12:31:28 +0000 |
| commit | c7e6c7ed183282b4a2cb2c679a8f5f51a2dc04c1 (patch) | |
| tree | d440163f5ffa8782069cd83fbcda04a2d146e53a /ci.sh | |
| parent | 98398d31f7d9bbda06fbb97804ba6844298710bc (diff) | |
| parent | 046a99aba01051c93d2f6a4d2f6e54ddde4f7fd4 (diff) | |
Merge pull request #1521 from embassy-rs/ci-doc
Move doc building to new CI.
Diffstat (limited to 'ci.sh')
0 files changed, 0 insertions, 0 deletions