Simplify all.do script.

diff --git a/processor/all.do b/processor/all.do
index 5857254a2c72b56f801833bac0161861d81a15f4..e448a44fac615a12ae7f94581d6b2965805cc041 100644 (file)
--- a/processor/all.do
+++ b/processor/all.do
@@ -36,12 +36,7 @@ done
 for file in *.rst *.md; do
   if test -f "$file"; then
     redo-ifchange "${metadata_dir}/${file%.*}.intermediate"
-  fi
-done
-for file in "$metadata_dir"/*.intermediate; do
-  if test -f "$file"; then
-    basename=$(basename "$file")
-    html_file=${basename%.intermediate}.html
+    html_file=${file%.*}.html
     redo-ifchange "$html_file"
     ln -sf "$cur_dir/$html_file" "${public_dir}/"
   fi