Add dev-docs to check_for_changes script

Changes to dev-docs are now identified as doc changes so builds can be skipped if necessary.

buildconfig/Jenkins/check_for_changes

@@ -40,7 +40,7 @@ case "$TYPE" in
 	# FOUND=1 iff changes are limited to docs or GUI only
 	# Find all changed files and grep for required type. -v inverts match so grep=0 means
 	# there are other changes besides this
-	if git diff --name-only ${BRANCH_TIP} ${BRANCH_BASE} -- | grep -q -E -v '^docs/|^qt/|^MantidPlot/'; then
+	if git diff --name-only ${BRANCH_TIP} ${BRANCH_BASE} -- | grep -q -E -v '^docs/|^dev-docs/|^qt/|^MantidPlot/'; then
 	    exit $FOUND
 	else
 	    exit $NOTFOUND