docs/tools/make_pages.sh | raw changeset files shortlog |
1.1 --- a/docs/tools/make_pages.sh Fri Nov 24 17:24:23 2017 +0100 1.2 +++ b/docs/tools/make_pages.sh Mon Apr 15 00:13:49 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" = "imip-agent" ]; then 1.9 PAGENAME="$PREFIX" 1.10 else 1.11 PAGENAME="$PREFIX/$PAGENAME"