X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Fcommand.c;h=c6d7659d09c1c34632487b1df8142c211e508171;hb=65e4b2dda3939a9c35913a79b7e79c3120713a6c;hp=0d557b2092e2c096e7ebfe21b68d6d86d33b8956;hpb=40271dcbfdecb01dfe808684741215eb2ddeb508;p=pspp

diff --git a/src/command.c b/src/command.c
index 0d557b2092..c6d7659d09 100644
--- a/src/command.c
+++ b/src/command.c
@@ -739,7 +739,7 @@ shell (void)
 	
 	execl (shell_fn, shell_process, NULL);
 
-	err_hcf (1);
+	_exit (1);
       }
 
     case -1: