devtools repo

[Jim Jagielski]

The `devtools` repo is still hosted under svn... should we migrate it to git?
--
Jim
            "If you can dodge a wrench, you can dodge a ball."