Skip to content

Conversation

9rnsr
Copy link
Contributor

@9rnsr 9rnsr commented Aug 19, 2014

@quickfur
Copy link
Member

LGTM.

@quickfur
Copy link
Member

Auto-merge toggled on

@jmdavis
Copy link
Member

jmdavis commented Aug 19, 2014

Ah, drat. Sorry about that. Thanks for taking care of that Kenji.

@quickfur
Copy link
Member

Hmph. Looks like there are merge conflicts. Ping @9rnsr

@9rnsr
Copy link
Contributor Author

9rnsr commented Aug 19, 2014

What?

@9rnsr
Copy link
Contributor Author

9rnsr commented Aug 19, 2014

PR is was automatically merged, but this page does not reflect it....

@quickfur
Copy link
Member

Huh, that's weird. I've never seen that happen before. How do we fix that? Just close the PR manually?

quickfur pushed a commit to quickfur/phobos that referenced this pull request Aug 19, 2014
fix up issue 13313 - Support database name to Windows timezone name conversion
@jmdavis
Copy link
Member

jmdavis commented Aug 19, 2014

I guess so, though @braddr should probably know, since it implies that there's a bug somewhere if a PR gets merged by the autotester without github knowing about it.

@braddr
Copy link
Member

braddr commented Aug 19, 2014

looks like github timed out the merge and it's github itself that's in an odd state. just going to close this pull since it's merged.

@braddr braddr closed this Aug 19, 2014
@9rnsr 9rnsr deleted the fix_timezone branch August 20, 2014 00:35
9rnsr pushed a commit to 9rnsr/phobos that referenced this pull request Aug 25, 2014
fix up issue 13313 - Support database name to Windows timezone name conversion
9rnsr pushed a commit to 9rnsr/phobos that referenced this pull request Sep 1, 2014
fix up issue 13313 - Support database name to Windows timezone name conversion
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants