equal
deleted
inserted
replaced
1346 |
1346 |
1347 "Modified: / 27-10-2018 / 19:16:00 / Claus Gittinger" |
1347 "Modified: / 27-10-2018 / 19:16:00 / Claus Gittinger" |
1348 ! |
1348 ! |
1349 |
1349 |
1350 openDocumentation |
1350 openDocumentation |
|
1351 "Called when <F1> is pressed" |
|
1352 |
1351 HTMLDocumentView openFullOnDocumentationFile:'tools/misc/TOP.html#INSPECTOR'. |
1353 HTMLDocumentView openFullOnDocumentationFile:'tools/misc/TOP.html#INSPECTOR'. |
1352 ! |
1354 ! |
1353 |
1355 |
1354 refreshTabs |
1356 refreshTabs |
1355 self navigationHistoryHolder currentItem refreshTabs. |
1357 self navigationHistoryHolder currentItem refreshTabs. |