GitHubでmergeしたはずのmasterがでぐれった話

GitHubで、pull requestしたbranchをmergeして
もらったので、早速masterをpullしてタグを付けて
pushしたんですね。

そんでブラウザで付けたタグを確認すると、ソースが
merge前のものになってたんです。

！？

焦ってmasterを見ると、ちゃんとmergeされている。
あれおっかしーなと思ってタグを削除して再度push
するもエラーが出てしまってうまくいかない。

...

ひとまず落ち着いてmasterを別ディレクトリにclone、
以下のページを参考にタグを付け直しました。

うまくいきました。

当たり前といえばそうなのですが、GitHubへのmergeの
反映に若干の遅延があるようです。

メンチカツ