From 6293380406eb5140531806b8dd07d3594f3e1229 Mon Sep 17 00:00:00 2001
From: Aparajita Fishman <aparajita@aparajita.com>
Date: Tue, 10 Apr 2012 22:42:46 -0400
Subject: [PATCH] Let jake proceed if a man page cannot be copied

---
 common.jake | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/common.jake b/common.jake
index d40edfa7c..720f7d923 100644
--- a/common.jake
+++ b/common.jake
@@ -489,10 +489,7 @@ global.copyManPage = function(/*String*/ name, /*int*/ section)
         if (!FILE.isDirectory(manDir))
         {
             if (sudo(["mkdir", "-p", "-m", "0755", manDir]))
-            {
                 stream.print("\0red(Unable to create the man directory.\0)");
-                OS.exit(1);
-            }
         }
 
         if (sudo(["cp", "-f", pageFile, manDir]))