diff options
Diffstat (limited to 'docs/check_pkgs')
| -rw-r--r-- | docs/check_pkgs | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/docs/check_pkgs b/docs/check_pkgs deleted file mode 100644 index 68fb76db12..0000000000 --- a/docs/check_pkgs +++ /dev/null @@ -1,20 +0,0 @@ - -silent_which () -{ - which $1 1>/dev/null 2>/dev/null || { - echo "=================================================" - echo "=================================================" - echo "= WARNING: Package '$1' is required" - echo "= to build Xen documentation" - echo "=================================================" - echo "=================================================" - } - which $1 1>/dev/null 2>/dev/null -} - -silent_which latex || exit 1 -silent_which dvips || exit 1 -silent_which ps2pdf || exit 1 -silent_which fig2dev || exit 1 - -exit 0 |