Merging GitHub pull requests from the command line

I just tested it, because I wasn’t sure.  As of 2018-12-09:

  • If you use git merge to merge a pull request (PR) from the command line, GitHub will detect that the PR’s commit(s) have been added to master, and will automatically mark the PR as “merged”.
  • If you instead use git rebase to move the PR branch onto master, GitHub will not automatically mark the PR as merged.

This makes sense, because rebase doesn’t actually modify the existing commit(s) in the PR.  Instead, it creates new commit(s) that make the same changes the PR’s commits would have made if merged.  So if you want to rebase or squash, do so from the Web interface.  (Or, alternatively, this tool and its corresponding blog post — although please note that I haven’t tried it myself.  Let me know if you do!)

I tried these with PRs in a single repo.  Please chime in if you have any experience with merging PRs from a fork into a parent.

(And one final note: I discovered the hard way that git rebase won’t preserve empty commits.  That is because it cares about the changes, so a commit that makes no changes isn’t of interest to rebase.)


I installed Rakudo Star

It’s the reference implementation of the Raku programming language.

The installer ran very quickly and the REPL worked out of the box. Nothing else to report yet, but I’m sure I’ll have more to say in the future.

Happy hacking!

Updated 1: Rakudo won’t build from source on Cygwin because libuv is still a bit dicey there.  However, cascent/neovim-cygwin looks like a promising step forward.

Music of the Day

“Treason” by Gryphon, released in 1977.  I’ve just started the third consecutive play of this record, so I think it’s time to give it the recognition it deserves!  The opener, “Spring Song,” is fantastic.  “Flash in the Pantry” is light and enjoyable.  High-grade prog.


By the way, my thanks to the WordPress team for clearing out the spam-followers that have been popping up over the last several months.  I appreciate it!

How to delete all the animations in a PowerPoint presentation using VBA

Very useful! This answer is copied from here. I tried to archive it, but wasn’t able to save it for some reason. I am posting it here so it can be archived for posterity.

answerspleasee asked on October 19, 2010
 How to delete all the animations in a presentation

how do I delete all animations i have put on for the past 200 slides.


Shyam Pillai replied on October 19, 2010

You can turn off the animations by going to Setup Slide Show and under Show Options tick the Show without animation option and click OK. Now run the show and it will display without the animations.

If you really want to delete all the animations in a single sweep then you will need to run this macro.

Sub StripAllBuilds()
 Dim I As Integer: Dim J As Integer
 Dim oActivePres As Object
 Set oActivePres = ActivePresentation
 With oActivePres
 For I = 1 To .Slides.Count
 If val(Application.Version) < 10 Then
 ' Older versions of PowerPoint 97/2000
 ' In each slide set the animation property
 ' of the Shape object to FALSE
 For J = 1 To .Slides(I).Shapes.Count
 .Slides(I).Shapes(J).AnimationSettings.Animate = msoFalse
 Next J
 ' New versions support the Timeline object
 For J = .Slides(I).TimeLine.MainSequence.Count To 1 Step -1
 Next J
 End If
 Next I
 End With
 Set oActivePres = Nothing
End Sub

Regards, Shyam Pillai.
 Shyam Pillai