get_filetime(): ページが存在しないときに0を返すように

diff --git a/file.php b/file.php
index 50f6244..b4f9ecd 100644 (file)
--- a/file.php
+++ b/file.php
@@ -2,7 +2,7 @@
 /////////////////////////////////////////////////
 // PukiWiki - Yet another WikiWikiWeb clone.
 //
-// $Id: file.php,v 1.27 2003/07/14 03:54:24 arino Exp $
+// $Id: file.php,v 1.28 2003/07/22 05:28:16 arino Exp $
 //
 
 // ¥½¡¼¥¹¤ò¼èÆÀ
@@ -18,6 +18,10 @@ function get_source($page=NULL)
 // ¥Ú¡¼¥¸¤Î¹¹¿·»þ¹ï¤òÆÀ¤ë
 function get_filetime($page)
 {
+       if (!is_page($page))
+       {
+               return 0;
+       }
        return filemtime(get_filename($page)) - LOCALZONE;
 }