--- a/src/user-prefs.cc	Fri Dec 08 21:57:50 1995 +0000
+++ b/src/user-prefs.cc	Fri Dec 08 22:08:48 1995 +0000
@@ -67,6 +67,7 @@
   user_pref.resize_on_range_error = 0;
   user_pref.return_last_computed_value = 0;
   user_pref.save_precision = 0;
+  user_pref.saving_history = 0;
   user_pref.silent_functions = 0;
   user_pref.split_long_rows = 0;
   user_pref.struct_levels_to_print = 0;
@@ -409,6 +410,17 @@
 }
 
 
+// Should we save command history?
+
+int
+saving_history (void)
+{
+  user_pref.saving_history = check_preference ("saving_history");
+
+  return 0;
+}
+
+
 // Suppress printing results in called functions.
 
 int