diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Info.plist | 6 | ||||
-rwxr-xr-x | src/index.sh | 29 |
2 files changed, 31 insertions, 4 deletions
diff --git a/src/Info.plist b/src/Info.plist index 111baae..b8645ff 100644 --- a/src/Info.plist +++ b/src/Info.plist @@ -3,11 +3,11 @@ <plist version="1.0"> <dict> <key>CFBundleIdentifier</key> - <string><!-- VALUE --></string> + <string>flex</string> <key>CFBundleName</key> - <string><!-- VALUE --></string> + <string>Flex</string> <key>DocSetPlatformFamily</key> - <string><!-- VALUE --></string> + <string>flex</string> <key>isDashDocset</key> <true/> </dict> diff --git a/src/index.sh b/src/index.sh index 35ed08c..5aca876 100755 --- a/src/index.sh +++ b/src/index.sh @@ -13,10 +13,23 @@ get_title() { FILE="$1" pup -p -f "$FILE" 'title text{}' | \ + sed 's/(Lexical Analysis With Flex.*)//' | \ tr -d \\n | \ sed 's/\"/\"\"/g' } +get_type() { + PAGE_NAME="$1" + + case "$PAGE_NAME" in + option-*) + echo "Option" + ;; + *) + echo "Guide" + esac +} + insert() { NAME="$1" TYPE="$2" @@ -31,7 +44,21 @@ insert_pages() { unset PAGE_NAME unset PAGE_TYPE PAGE_NAME="$(get_title "$1")" - PAGE_TYPE="Guide" + + # determine type + case "$PAGE_NAME" in + option-*) + PAGE_TYPE="Option" + PAGE_NAME="$(echo "$PAGE_NAME" | sed 's/^option-//')" + ;; + unnamed-* | deleteme* | ERASEME*) + shift + continue + ;; + *) + PAGE_TYPE="Guide" + esac + if [ -n "$PAGE_NAME" ]; then insert "$PAGE_NAME" "$PAGE_TYPE" "$(basename "$1")" fi |