[GRASS-dev] POSIX Shell vs. $(), local, and test

[Ivan Shmakov]

>>>>> Ivan Shmakov <ivan at theory.asu.ru> writes:
>>>>> Markus Neteler <neteler at osgeo.org> writes:

 >>> Take a look at the minor change for lib/insert_raster.sh as well
 >>> (attached.)

 >> Looks much more polished. But it looks like bash to me, right?  So
 >> far we try to avoid bash-isms in GRASS for portability.  Or will it
 >> run with ash, too?

 > It seems that both `local' and `$(COMMAND)' are available in either
 > `dash' or BusyBox' `ash', e. g.:

[...]

 > It's probably reasonable to require a Shell implementation with
 > either once you're depending on Shell functions being available.

 > I'm not sure that these constructs are mandated by any standard,
 > though.

	Apparently, the $(COMMAND) substitution is mandated by IEEE Std
	1003.1 (AKA POSIX) [1].  On the contrary, the `local' keyword
	isn't available as per [2].

 > The `test' (`[ ... ]') command should be generally available as well.
 > IIRC, it's mandated by POSIX.

	The `test X -lt Y' form is also available [3].

	Hence, I suggest the attached patch instead of the former one.

[...]

[1] http://www.opengroup.org/onlinepubs/009695399/utilities/xcu_chap02.html#tag_02_06_03
[2] http://www.opengroup.org/onlinepubs/009695399/utilities/xcu_chap02.htm
[3] http://www.opengroup.org/onlinepubs/009695399/utilities/test.html
-------------- next part --------------
--- lib/insert_raster.sh	2008-01-13 02:06:37.000000000 +0600
+++ lib/insert_raster.sh	2008-01-13 21:57:52.000000000 +0600
@@ -9,28 +9,19 @@
 #pasre the grass date format and convert it into sqlite date format
 parse_timestamp() #arguments are DAY MONTH YEAR TIME
 {
-DAY=$1
-MONTH=$2
-YEAR=$3
-TIME=$4
-
-# change the month to MM!!!! :/
-MONTH=`echo $MONTH | sed s/Jan/01/`
-MONTH=`echo $MONTH | sed s/Feb/02/`
-MONTH=`echo $MONTH | sed s/Mar/03/`
-MONTH=`echo $MONTH | sed s/Apr/04/`
-MONTH=`echo $MONTH | sed s/May/05/`
-MONTH=`echo $MONTH | sed s/Jun/06/`
-MONTH=`echo $MONTH | sed s/Jul/07/`
-MONTH=`echo $MONTH | sed s/Aug/08/`
-MONTH=`echo $MONTH | sed s/Sep/09/`
-MONTH=`echo $MONTH | sed s/Oct/10/`
-MONTH=`echo $MONTH | sed s/Nov/11/`
-MONTH=`echo $MONTH | sed s/Dec/12/`
-#change the day to DD
-if [ `expr $DAY \< 10` -eq 1 ] ; then
-DAY="0$DAY"
-fi
+    DAY=$1 ; MONTH=$2 ; YEAR=$3 ; TIME=$4
+
+    # change the month to MM!!!! :/
+    MONTH=$(echo "$MONTH" \
+                | sed -e s/Jan/01/ -e s/Feb/02/ -e s/Mar/03/ \
+                      -e s/Apr/04/ -e s/May/05/ -e s/Jun/06/ \
+                      -e s/Jul/07/ -e s/Aug/08/ -e s/Sep/09/ \
+                      -e s/Oct/10/ -e s/Nov/11/ -e s/Dec/12/)
+
+    # change the day to DD
+    if [ $DAY -lt 10 ] ; then
+        DAY="0$DAY"
+    fi
 
 GLOBAL_DATE_VAR="$YEAR-$MONTH-$DAY $TIME"
 }