Merge pull request #132 from davidgiven/dtrg-mips
authorDavid Given <dg@cowlark.com>
Sat, 22 Sep 2018 10:04:13 +0000 (11:04 +0100)
committerGitHub <noreply@github.com>
Sat, 22 Sep 2018 10:04:13 +0000 (11:04 +0100)
commitc6a1cf8de457369132cfb1b6f5411413d671e43f
treebae0a38eabc4be560c8ba333683e45f153738d3b
parent8fd3e1f5ced8221a99c08043f277070c0d8b99cd
parent79e7636537d0738014074ac1d4df7e9a0ca415ea
Merge pull request #132 from davidgiven/dtrg-mips

Teach mcg how to merge pushes