# HG changeset patch
# User jwe
# Date 831139607 0
# Node ID 0ef10ffb18eb48d51210dbfb819d83d930fb62ee
# Parent  320f5463c2012ecbe8693747d48af66547500edb
[project @ 1996-05-03 16:06:47 by jwe]

diff -r 320f5463c201 -r 0ef10ffb18eb src/user-prefs.cc
--- a/src/user-prefs.cc	Fri May 03 01:20:05 1996 +0000
+++ b/src/user-prefs.cc	Fri May 03 16:06:47 1996 +0000
@@ -996,15 +996,7 @@
 {
   int status = 0;
 
-  string s = builtin_string_variable ("PS1");
-
-  if (s.empty ())
-    {
-      gripe_invalid_value_specified ("PS1");
-      status = -1;
-    }
-  else
-    user_pref.ps1 = s;
+  user_pref.ps1 = builtin_string_variable ("PS1");
 
   return status;
 }
@@ -1014,15 +1006,7 @@
 {
   int status = 0;
 
-  string s = builtin_string_variable ("PS2");
-
-  if (s.empty ())
-    {
-      gripe_invalid_value_specified ("PS2");
-      status = -1;
-    }
-  else
-    user_pref.ps2 = s;
+  user_pref.ps2 = builtin_string_variable ("PS2");
 
   return status;
 }
@@ -1032,15 +1016,7 @@
 {
   int status = 0;
 
-  string s = builtin_string_variable ("PS4");
-
-  if (s.empty ())
-    {
-      gripe_invalid_value_specified ("PS4");
-      status = -1;
-    }
-  else
-    user_pref.ps4 = s;
+  user_pref.ps4 = builtin_string_variable ("PS4");
 
   return status;
 }