@@ -513,7 +513,7 @@ public void saveFile() {
513
513
*/
514
514
public void keyPressed (KeyEvent e ) {
515
515
// Preferences for the "input file"
516
- PreferencesPanel .setProperty (prefsIO , e .getSource ());
516
+ PreferencesPanel .setProperty (prefsIO , e .getSource (), true );
517
517
}
518
518
519
519
/*
@@ -523,7 +523,7 @@ public void keyPressed(KeyEvent e) {
523
523
*/
524
524
public void keyReleased (KeyEvent e ) {
525
525
// Preferences for the "input file"
526
- PreferencesPanel .setProperty (prefsIO , e .getSource ());
526
+ PreferencesPanel .setProperty (prefsIO , e .getSource (), true );
527
527
}
528
528
529
529
/*
@@ -533,7 +533,7 @@ public void keyReleased(KeyEvent e) {
533
533
*/
534
534
public void keyTyped (KeyEvent e ) {
535
535
// Preferences for the "input file"
536
- PreferencesPanel .setProperty (prefsIO , e .getSource ());
536
+ PreferencesPanel .setProperty (prefsIO , e .getSource (), true );
537
537
}
538
538
539
539
/*
@@ -544,7 +544,7 @@ public void keyTyped(KeyEvent e) {
544
544
*/
545
545
public void itemStateChanged (ItemEvent e ) {
546
546
// Preferences for the "output format"
547
- PreferencesPanel .setProperty (prefsIO , e .getSource ());
547
+ PreferencesPanel .setProperty (prefsIO , e .getSource (), true );
548
548
}
549
549
550
550
/*
0 commit comments