| Index: devtools-panel.html |
| diff --git a/devtools-panel.html b/devtools-panel.html |
| index b66ad24ba14b4a9c7c2948f2d2ff90a1010045ba..59c554b1d2d368025fe95e344633a2a5e415d803 100644 |
| --- a/devtools-panel.html |
| +++ b/devtools-panel.html |
| @@ -53,6 +53,7 @@ |
| <option>PING</option> |
| <option>POPUP</option> |
| <option>ELEMHIDE</option> |
| + <option>WEBSOCKET</option> |
| <option>OTHER</option> |
| </select> |
| type |