X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;ds=sidebyside;f=src%2Fset.q;h=620961b59ca46415e50647625aa76feed43ca0b5;hb=a6ae02832bc0e093c2d21fe2534d9f90677803dd;hp=b6bcb23f7a5aa36a5fdcb06113df5c393e4a1ae6;hpb=f62199cac6213ed1c03ffe48450a583da0fadc68;p=pspp

diff --git a/src/set.q b/src/set.q
index b6bcb23f7a..620961b59c 100644
--- a/src/set.q
+++ b/src/set.q
@@ -1054,13 +1054,15 @@ set_viewport(int sig_num UNUSED)
 void
 done_settings(void)
 {
-  free(set_pager);
-  free(set_journal);
+  if ( rng ) 
+    gsl_rng_free (rng);
+  free (set_pager);
+  free (set_journal);
 
-  free(cmd.s_endcmd);
-  free(cmd.s_prompt);
-  free(cmd.s_cprompt);
-  free(cmd.s_dprompt);
+  free (cmd.s_endcmd);
+  free (cmd.s_prompt);
+  free (cmd.s_cprompt);
+  free (cmd.s_dprompt);
 }
 
 
@@ -1102,10 +1104,18 @@ init_settings(void)
 
 #if !USE_INTERNAL_PAGER
   {
-    char *pager;
+    const char *pager = getenv ("STAT_PAGER");
 
-    pager = getenv ("STAT_PAGER");
-    if (!pager)  set_pager = getenv ("PAGER");
+    if (!pager) 
+      {
+	const char *p = getenv ("PAGER");
+	
+	if ( p != NULL ) 
+	  set_pager = xstrdup (p);
+	else
+	  set_pager = 0;
+      }
+    
 
     if (pager)  
       set_pager = xstrdup (pager);