# HG changeset patch
# User jwe
# Date 782068435 0
# Node ID b7d68dfee8d817f8e123efbb31748da759486bd8
# Parent  cbc37d8d0fdfb112d69d2de3860dcf054058a409
[project @ 1994-10-13 17:13:55 by jwe]

diff -r cbc37d8d0fdf -r b7d68dfee8d8 scripts/miscellaneous/bug_report.m
--- a/scripts/miscellaneous/bug_report.m	Thu Oct 13 17:03:45 1994 +0000
+++ b/scripts/miscellaneous/bug_report.m	Thu Oct 13 17:13:55 1994 +0000
@@ -57,4 +57,8 @@
 
   system (sprintf ("%s > /dev/tty", cmd));
 
+  if (! isempty (prefs))
+    system (sprintf ("rm -f %s", prefs));
+  endif
+
 endfunction