Files
mediawiki-extensions-Univer…/scripts/update-jquery-ime.sh
Kartik Mistry f25fca0dcb Check if directory exists in a better manner
* This avoids warnings like: line 8: cd: /tmp/jquery.ime:
   No such file or directory.
 * Formatting fixes.

Change-Id: Icbc3f6f80314cae3ea9b5dfdc3e66c59af225621
2014-02-11 17:39:24 +05:30

21 lines
404 B
Bash
Executable File

#!/bin/bash
DEST="../lib/jquery.ime";
CLONEDIR="/tmp/jquery.ime";
HERE=`pwd`;
UPSTREAM="https://github.com/wikimedia/jquery.ime.git";
echo -e "Getting latest jquery.ime from $UPSTREAM\n";
if [ -d $CLONEDIR ]; then
git pull;
else
git clone $UPSTREAM $CLONEDIR;
fi
cd $CLONEDIR;
npm install;
grunt copy concat;
cd $HERE;
cp -rf $CLONEDIR/dist/jquery.ime/{images,css,rules,jquery.ime.js} $DEST;