Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Ignore error if nothing to commit #396

Merged
merged 1 commit into from
Dec 2, 2022
Merged

Ignore error if nothing to commit #396

merged 1 commit into from
Dec 2, 2022
+1 −1

Conversation

jdahm
Copy link
Contributor

@jdahm jdahm commented Dec 2, 2022

Purpose

Fix push_docs by ignoring error if there is nothing to commit.

I checked and git push returns 0 if there is nothing to push, so this should be all that is needed to avoid the test "failure".

@jdahm
Ignore error if nothing to commit

Verified

This commit was signed with the committer’s verified signature. The key has expired.
jdahm Johann Dahm
GPG key ID: 0C01D3D918A72694
Expired
Verified
Learn about vigilant mode
0b48801
@jdahm jdahm requested a review from elynnwu December 2, 2022 05:54
@FlorianDeconinck
Copy link
Contributor

launch jenkins

elynnwu
elynnwu approved these changes Dec 2, 2022
View reviewed changes
Copy link
Collaborator

@elynnwu elynnwu left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

lgtm

@FlorianDeconinck FlorianDeconinck merged commit 0620667 into main Dec 2, 2022
@FlorianDeconinck FlorianDeconinck deleted the fix-push-docs branch December 2, 2022 19:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@elynnwu elynnwu

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@jdahm @FlorianDeconinck @elynnwu