/* Read in the preferences. */
$highlight_num = 0;
while (! feof($file)) {
- $pref = trim(fgets($file, 1024));
+ // Make sure that this fgets is larger than any of the pref strings
+ // could ever be. 1024 is too short
+ $pref = trim(fgets($file, 65536));
$equalsAt = strpos($pref, '=');
if ($equalsAt > 0) {
$key = substr($pref, 0, $equalsAt);
$value = substr($pref, $equalsAt + 1);
+ /* this is to 'rescue' old-style highlighting rules. */
if (substr($key, 0, 9) == 'highlight') {
$key = 'highlight' . $highlight_num;
$highlight_num ++;