Changeset 10a85fe in git

Timestamp:

May 2, 2011, 6:55:13 PM (12 years ago)

Author:

Oleksandr Motsak <motsak@…>

Branches:

(u'jengelh-datetime', 'ceac47cbc86fe4a15902392bdbb9bd2ae0ea02c6')(u'spielwiese', '0604212ebb110535022efecad887940825b97c3f')

Children:

3bb9cb2aa362f52992e1584a41e4f67368e603b3

Parents:

3033f07edbebc827dd4bf79ffda980b3f5a6ba50

git-author:

Oleksandr Motsak <motsak@mathematik.uni-kl.de>2011-05-02 18:55:13+02:00

git-committer:

Mohamed Barakat <mohamed.barakat@rwth-aachen.de>2011-11-09 12:31:32+01:00

Message:

ADD: better 'date' format (no spaces)
ADD: paralell run-protection
ADD: build dir is date-dependent
CHG: no default "-j" make option

File:

• sw.sh (modified) (3 diffs)

sw.sh

@@ -3 +3 @@
 PWD=`pwd`
 BRANCH="spielwiese"
+
+# configure' options
 CFGOPTIONS="--with-gmp=yes"
-MKOPTIONS="-j9"
+
+# computer specific make options: e.g. -j9
+#MKOPTIONS="-j9"
+MKOPTIONS="" 
+
+D=`date +%y.%m.%d.%H.%M.%S`
+
 # tempdir (absolute path!)
-SW="$PWD/SW"
+SW="$PWD/SW_$D.dir"
 
 # we try to use log instead of consequent --quiet
-LOG="$PWD/`date`.log"
+LOG="$PWD/SW_$D.log"
 
 # log or no log?
@@ -15 +23 @@
 
 echo "DATE: `date`" >> $LOG
+echo "HOST: `hostname`" >> $LOG
+echo "SYSTEM: `uname -a`" >> $LOG 
+
 
 CleanUp() 
 {
   echo "Deleting tempdir: $SW" >> $LOG
-  rm -f -R $SW 1>> $LOG 2>&1
+  rm -f -R "$SW" 1>> $LOG 2>&1
 }
 
@@ -59 +70 @@
 
 echo "Creating empty tempdir: $SW" >> $LOG
-[ -d $SW ] && { echo "Error: $SW exists... cleaning up..." >> $LOG; CleanUp; }
+[ -d $SW ] && { echo "Error: $SW exists... cleaning up..." >> $LOG; mv -f $SW "$SW.moved" 1>> $LOG 2>&1 && { rm -f -R "$SW.moved" 1>> $LOG 2>&1 || echo "Error: could not remove '$SW.moved'"; } || { echo "Error: could not rename '$SW' -> '$SW.moved'"; exit 1; };  }
 
 mkdir -p $SW || { echo "Error: cannot create tempdir: $SW" >> $LOG;  exit 1; }