diff options
| -rw-r--r-- | gui/TabWidget.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/gui/TabWidget.h b/gui/TabWidget.h index 7e4c1d8139..928f7916b6 100644 --- a/gui/TabWidget.h +++ b/gui/TabWidget.h @@ -72,6 +72,10 @@ public: * Remove the tab with the given tab ID. Disposes all child widgets of that tab. * TODO: This code is *unfinished*. In particular, it changes the * tabIDs, so that they are not unique anymore! This is bad. + * If we need to, we could fix this by changing the tab IDs from being an index + * into the _tabs array to a real "unique" ID, which gets stored in the Tab struct. + * It won't be difficult to implement this, but since currently no code seems to make + * use of the feature... */ void removeTab(int tabID); |