private DataTypeManager userChooseDataTypeManager() {
		PluginTool tool = state.getTool();
		DataTypeManagerService service = tool.getService(DataTypeManagerService.class);
		DataTypeManager[] dataTypeManagers = service.getDataTypeManagers();
		String names[] = new String[dataTypeManagers.length];
		String initialDtmChoice = names[0];
		try {
			initialDtmChoice = currentProgram.getDataTypeManager().getName();
		}
		catch (Exception e) {
			// Ignore... assuming no program or dtm.
		}
		for (int i = 0; i < dataTypeManagers.length; i++) {
			names[i] = dataTypeManagers[i].getName();
		}
		String userChoice =
			OptionDialog.showInputChoiceDialog(null, "Choose a Data Type Manager or Cancel",
				"Choose", names, initialDtmChoice, OptionDialog.PLAIN_MESSAGE);
		if (userChoice == null) {
			return null;
		}
		for (int i = 0; i < dataTypeManagers.length; i++) {
			if (names[i].contentEquals(userChoice)) {
				return dataTypeManagers[i];
			}
		}
		return null; // should not reach this line.
	}
A method to remove characters from the given string that are output by the HTML
conversion process when going from HTML to plain text.

@param s the string to be updated
@return the updated String
Ghidra/Features/PDB/developer_scripts/DeveloperDumpAllTypesScript.java