From 97af158927ca9847b3777c503c38474e1ecf582c Mon Sep 17 00:00:00 2001 From: "John J. Camilleri" Date: Sat, 9 Jun 2018 20:44:00 +0200 Subject: [PATCH] Minor fix in RGL browser --- doc/browse/.gitignore | 1 + doc/browse/build-tags.sh | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) create mode 100644 doc/browse/.gitignore mode change 100644 => 100755 doc/browse/build-tags.sh diff --git a/doc/browse/.gitignore b/doc/browse/.gitignore new file mode 100644 index 000000000..c41ecfbda --- /dev/null +++ b/doc/browse/.gitignore @@ -0,0 +1 @@ +tags/*.gf-tags diff --git a/doc/browse/build-tags.sh b/doc/browse/build-tags.sh old mode 100644 new mode 100755 index 3a0fec900..49a7e5089 --- a/doc/browse/build-tags.sh +++ b/doc/browse/build-tags.sh @@ -49,7 +49,7 @@ do $FIND | while read -r file do echo " \""`echo $file | sed 's|./||;s|.gf||'`"\"," >> $index - filemtime=`$STAT "${tagsdir}/${file}-tags"` 2>/dev/null + filemtime=`$STAT "${tagsdir}/${file}-tags" 2>/dev/null` if [ -z "$filemtime" ] || [ "$filemtime" -lt "$start" ] then gf --batch --quiet --tags --output-dir=${tagsdir} $file 2>/dev/null