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

Make it easier to find the documentation on the date string format #437

Merged
merged 3 commits into from
Mar 2, 2017
Merged

Make it easier to find the documentation on the date string format #437

merged 3 commits into from
Mar 2, 2017

Conversation

benjamingeer
Copy link

Closes #431.

@benjamingeer benjamingeer added the enhancement improve existing code or new feature label Feb 28, 2017
@benjamingeer benjamingeer added this to the Beta Release milestone Feb 28, 2017
@tobiasschweizer
Copy link
Contributor

This is fine.

Could you check if we also need to add || true after git commit in update-gh-pages.sh?
I think if this is not added and nothing was actually changed to be committed, the script would terminate with -1, not switching back to develop.

@tobiasschweizer
Copy link
Contributor

This PR can be merged!

@benjamingeer benjamingeer merged commit ce8de44 into develop Mar 2, 2017
@benjamingeer benjamingeer deleted the wip/date-format-doc branch March 2, 2017 13:27
@benjamingeer benjamingeer mentioned this pull request Jul 5, 2019
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tobiasschweizer tobiasschweizer tobiasschweizer approved these changes

Assignees

@benjamingeer benjamingeer

@tobiasschweizer tobiasschweizer

Labels
enhancement improve existing code or new feature
Projects
None yet
Milestone
Beta Release
Development

Successfully merging this pull request may close these issues.
3 participants
@benjamingeer @tobiasschweizer @kilchenmann