PR #18790 ci/docs: create PR only if needed

ci/docs: create PR only if needed #18790

Borda merged 4 commits into master from ci/tutorials

ci/docs: create PR only if needed

c0f32b8e

Borda requested a review from

carmocca 2 years ago

Borda requested a review from

ethanwharris 2 years ago

Borda requested a review from

justusschock 2 years ago

github-actions added ci

[pre-commit.ci] auto fixes from pre-commit.com hooks

b54fdd2f

fix $

2428488c

Merge branch 'master' into ci/tutorials

43fed8d3

awaelchli approved these changes on 2023-10-13

justusschock approved these changes on 2023-10-13

mergify added ready

Borda merged a2377e9d into master 2 years ago

Borda deleted the ci/tutorials branch 2 years ago

awaelchli added this to the 2.1.x milestone 2 years ago

Reviewers

justusschock

awaelchli

carmocca

ethanwharris

Assignees

No one assigned

Labels

ready ci

Milestone

2.1.x