-
- $path = "$dir/$file";
-
- if (is_file($path)) {
- $pi = pathinfo($path);
- /* ignore files not ending in .md */
- if (!isset($pi["extension"]) || $pi["extension"] != "md") {
- continue;
- }
- if (!is_dir("$dir/".$pi["filename"])) {
- continue;
- }
- } else {
- /* ignore directories where an companying file exists */
- if (is_file("$path.md")) {
- continue;
- }
- }
-
- printf("<li>⇒ <a href=\"/%s\">%s</a></li>\n",
- urlpath($dir, $file),
- ns("$dir/".basename($file, ".md")));