extern/bat-extras
1
0
Fork 0
mirror of https://github.com/eth-p/bat-extras.git synced 2025-06-20 11:47:43 +02:00
Code Issues Packages Projects Releases Wiki Activity

build: Allow manuals to be disabled with --manuals=false

Browse Source
This commit is contained in:
Ethan P 2021-03-30 19:54:06 -07:00
parent cfd8d29c7b
commit 5f88acd1f4
No known key found for this signature in database
GPG Key ID: 6963FD04F6CF35EA
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
build.sh
View File

@ -379,7 +379,7 @@ while shiftopt; do
case "$OPT" in case "$OPT" in
--install) OPT_INSTALL=true ;; --install) OPT_INSTALL=true ;;
--compress) OPT_COMPRESS=true ;; --compress) OPT_COMPRESS=true ;;
--manuals) OPT_MANUALS=true ;; --manuals) OPT_MANUALS="${OPT_VAL:-true}" ;;
--no-manuals) OPT_MANUALS=false ;; --no-manuals) OPT_MANUALS=false ;;
--no-verify) OPT_VERIFY=false ;; --no-verify) OPT_VERIFY=false ;;
--no-banner) OPT_BANNER=false ;; --no-banner) OPT_BANNER=false ;;
@ -451,7 +451,7 @@ done
# ----------------------------------------------------------------------------- # -----------------------------------------------------------------------------
# Build manuals. # Build manuals.
if "$OPT_MANUALS"; then if [[ "$OPT_MANUALS" = "true" ]]; then
source "${HERE}/mdroff.sh" source "${HERE}/mdroff.sh"
if ! [[ -d "$MAN" ]]; then if ! [[ -d "$MAN" ]]; then
mkdir -p "$MAN" mkdir -p "$MAN"