# HG changeset patch
# User jwe
# Date 832005443 0
# Node ID 0bddc913621bcb0a8deeb7b4ff34ce1213df802c
# Parent  868d82fe5fdc79317edf6158bbc3641017f0db5a
[project @ 1996-05-13 16:36:11 by jwe]

diff -r 868d82fe5fdc -r 0bddc913621b src/help.cc
--- a/src/help.cc	Mon May 13 16:23:25 1996 +0000
+++ b/src/help.cc	Mon May 13 16:37:23 1996 +0000
@@ -44,6 +44,7 @@
 #include "dirfns.h"
 #include "error.h"
 #include "help.h"
+#include "input.h"
 #include "oct-obj.h"
 #include "pager.h"
 #include "pathsearch.h"
@@ -704,8 +705,8 @@
 
   begin_unwind_frame ("Ftype");
 
-  unwind_protect_str (user_pref.ps4);
-  user_pref.ps4 = "";
+  unwind_protect_str (Vps4);
+  Vps4 = "";
 
   int argc = args.length () + 1;
 
diff -r 868d82fe5fdc -r 0bddc913621b src/pt-pr-code.cc
--- a/src/pt-pr-code.cc	Mon May 13 16:23:25 1996 +0000
+++ b/src/pt-pr-code.cc	Mon May 13 16:37:23 1996 +0000
@@ -31,6 +31,7 @@
 #include <iostream.h>
 
 #include "error.h"
+#include "input.h"
 #include "pr-output.h"
 #include "pt-pr-code.h"
 #include "user-prefs.h"
@@ -1143,7 +1144,7 @@
  
   if (beginning_of_line)
     {
-      os.form ("%s%*s", user_pref.ps4.c_str (), curr_print_indent_level, "");
+      os.form ("%s%*s", Vps4.c_str (), curr_print_indent_level, "");
       beginning_of_line = false;
     }
 }