# HG changeset patch
# User jwe
# Date 818460528 0
# Node ID 50e71230d58254cc81029c67fc70007009583a04
# Parent  1f99a54d7b52b4fd0c6ceb62b6c5b37fefe1958e
[project @ 1995-12-08 22:07:30 by jwe]

diff --git a/src/oct-hist.cc b/src/oct-hist.cc
--- a/src/oct-hist.cc
+++ b/src/oct-hist.cc
@@ -64,9 +64,6 @@
 // Nonzero means input is coming from temporary history file.
 int input_from_tmp_history_file = 0;
 
-// Nonzero means we are saving history lines.
-int saving_history = 1;
-
 // The number of lines to save in the history file.
 static int octave_hist_size = 1024;
 
@@ -141,7 +138,7 @@
 void
 maybe_save_history (const char *s)
 {
-  if (saving_history)
+  if (user_pref.saving_history)
     {
       add_history (s);
       history_lines_this_session++;
diff --git a/src/oct-hist.h b/src/oct-hist.h
--- a/src/oct-hist.h
+++ b/src/oct-hist.h
@@ -35,9 +35,6 @@
 // Nonzero means input is coming from temporary history file.
 extern int input_from_tmp_history_file;
 
-// Nonzero means we are saving history lines.
-extern int saving_history;
-
 #endif
 
 /*
diff --git a/src/user-prefs.cc b/src/user-prefs.cc
--- a/src/user-prefs.cc
+++ b/src/user-prefs.cc
@@ -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