equal
deleted
inserted
replaced
235 "/usr/local/jedit" \ |
235 "/usr/local/jedit" \ |
236 "/usr/share/jedit" \ |
236 "/usr/share/jedit" \ |
237 "/opt/jedit" \ |
237 "/opt/jedit" \ |
238 "") |
238 "") |
239 |
239 |
240 JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx512m" |
240 JEDIT_JAVA_OPTIONS="" |
|
241 #JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx512m" |
241 JEDIT_OPTIONS="-reuseview -noserver -nobackground" |
242 JEDIT_OPTIONS="-reuseview -noserver -nobackground" |
242 |
243 |
243 |
244 |
244 ### |
245 ### |
245 ### External reasoning tools |
246 ### External reasoning tools |