devtools: various fixes

This commit is contained in:
Giacomo Tesio 2017-01-20 01:54:36 +01:00
parent 0e29b708cb
commit f6e1c78244
1 changed files with 1 additions and 1 deletions

@ -1 +1 @@
Subproject commit 7be0dbfbed31197cb7fdad141d3658064f81c2f9
Subproject commit ded9ac9fb9d9310e0ca6203513373f729eacf250