#!/bin/sh

set -e

. $(dirname $0)/../lib/sh/init

echo "Changing permissions of ${DVICORE_SCRIPT_BASE_DIR}/bin"
# We test the existence of the file dvibrowser in order to
# make sure that we have a correct directory.
if [ -f "${DVICORE_SCRIPT_BASE_DIR}/bin/dvibrowser" ] ; then
  for f in ${DVICORE_SCRIPT_BASE_DIR}/bin/* ; do
    echo "Fixing permission of $f"
    chmod a+x $f
  done
else
  echo "error: Unable to find dvibrowser launching script."
  exit 1
fi
