Community
Participate
Working Groups
The "JUnit plugin tests to TPTP" widget in the Import dialog (i.e File > Import...) should read "JUnit plug-in tests to TPTP". That is "plugin" should be changed to "plug-in" Note: if this bug is resolved corresponding screen shots need to be updated in the documentation as per https://bugs.eclipse.org/bugs/show_bug.cgi?id=114792.
Another point to append to this bug: The title bar of the "JUnit pluging tests to TPTP" wizard reads "JUnit pluging tests to TPTP Import Wizard". It should probably read "JUnit pluging tests to TPTP".
Fixed. Changed all occurrences of "plugin(s)" by "plug-in(s)". Also changed the wizard title, to be consistent with eclipse guidelines ("JUnit plugin tests to TPTP" replaced with "Import plug-in tests to TPTP"). Impacted UI elements: Import wizard, New wizard, Test navigator, Test Suite editor, Launch Configuration.
ACTION: Please verify/close this defect.
Closing by default since not closed by the originator in the 7+ months since being resolved. Please reopen if the issue is still present in the latest TPTP release or the resolution is not correct.