docs/tools/make_pages.sh | raw changeset files shortlog |
1.1 --- a/docs/tools/make_pages.sh Mon Feb 04 18:30:28 2019 +0100 1.2 +++ b/docs/tools/make_pages.sh Sun Apr 14 19:31:45 2019 +0200 1.3 @@ -56,7 +56,7 @@ 1.4 BASENAME=`basename "$FILENAME"` 1.5 PAGENAME=`echo "$BASENAME" | sed 's/--/\//g'` 1.6 if [ "$PREFIX" ]; then 1.7 - if [ "$PAGENAME" = "FrontPage" ]; then 1.8 + if [ "$PAGENAME" = "Lichen" ]; then 1.9 PAGENAME="$PREFIX" 1.10 else 1.11 PAGENAME="$PREFIX/$PAGENAME"