lib/browser/GraphBrowser/GraphBrowser.java
changeset 12411 8a8ea71c79d3
parent 11876 6ac0627167ed
child 14981 e73f8140af78
equal deleted inserted replaced
12410:ef373ec6ade8 12411:8a8ea71c79d3
    98 							} else
    98 							} else
    99 								buf += c;
    99 								buf += c;
   100 						} else if (c == '<') {
   100 						} else if (c == '<') {
   101 							html = true;
   101 							html = true;
   102 							ctrl = text2[i+1];
   102 							ctrl = text2[i+1];
   103 							if ((ctrl == 'P') || (ctrl == 'B'))
       
   104 								text3[j++] = '\n';		
       
   105 						} else if (c == '>')
   103 						} else if (c == '>')
   106 							html = false;
   104 							html = false;
   107 						else if (!html)
   105 						else if (!html)
   108 							text3[j++] = c;
   106 							text3[j++] = c;
   109 					}
   107 					}