
<html>

  <head>

    <meta content="text/html; charset=windows-1252"

      http-equiv="Content-Type">

  </head>

  <body text="#000000" bgcolor="#FFFFFF">

    <div class="moz-cite-prefix">On 05/09/2016 11:39 PM, Fred Bricon

      wrote:<br>

    </div>

    <blockquote

cite="mid:CACvX+Kie1mK+g_A1XcvKUx_00=_kGOsxQhDAegKBtd7NbDwX9w@mail.gmail.com"

      type="cite">

      <div dir="ltr">

        <div class="gmail_extra">

          <div class="gmail_quote">If it works locally, then instead of

            pushing the local merge back to origin, it's still

            preferable to use the green button to see the PR merged, not

            closed, in GH.<br>

          </div>

        </div>

      </div>

    </blockquote>

    Using the Gerrit workflow (single commit, rebase it and "push

    --force" back to topic branch to update it) with GitHub PR works

    fine enough, so doing a local push or merge marks the PR as merged.<br>

    What's GitHub is missing is a "Squash and Rebase" button to update

    the PR.<br>

    <div class="moz-signature">-- <br>

      Mickael Istria<br>

      Eclipse developer at <a href="http://www.jboss.org/tools">JBoss,

        by Red Hat</a><br>

      <a href="http://mickaelistria.wordpress.com">My blog</a> - <a

        href="http://twitter.com/mickaelistria">My Tweets</a></div>

  </body>

</html>