Changeset 4049 for trunk/integration
- Timestamp:
- 01/23/08 18:29:19 (12 months ago)
- Location:
- trunk/integration
- Files:
-
- 14 modified
-
bplgt.sh (modified) (2 diffs)
-
ciaolgt.sh (modified) (2 diffs)
-
cxlgt.sh (modified) (3 diffs)
-
eclipselgt.sh (modified) (2 diffs)
-
gplgt.sh (modified) (2 diffs)
-
NOTES.txt (modified) (1 diff)
-
plclgt.sh (modified) (2 diffs)
-
qplgt.sh (modified) (2 diffs)
-
quintuslgt.sh (modified) (2 diffs)
-
sicstuslgt.sh (modified) (2 diffs)
-
swilgt.sh (modified) (2 diffs)
-
xsblgt.sh (modified) (2 diffs)
-
xsbmtlgt.sh (modified) (2 diffs)
-
yaplgt.sh (modified) (2 diffs)
Legend:
- Unmodified
- Added
- Removed
-
trunk/integration/bplgt.sh
r4036 r4049 1 #/bin/ sh1 #/bin/bash 2 2 3 3 ## ================================================================ … … 43 43 echo "to your Logtalk user directory!" 44 44 echo "Trying the default location for the Logtalk user directory..." 45 echo 45 46 export LOGTALKUSER=$HOME/logtalk 46 if [ -d "$LOGTALKUSER" ]; then 47 echo "... using Logtalk user directory found at $LOGTALKUSER" 47 fi 48 49 if [ -d "$LOGTALKUSER" ]; then 50 if ! [ -a "$LOGTALKUSER/VERSION.txt" ]; then 51 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 52 echo "Creating an up-to-date Logtalk user directory..." 53 cplgtdirs 48 54 else 49 echo "... Logtalk user directory not found at default location. Creating a" 50 echo "new Logtalk user directory by running the \"cplgtdirs\" shell script:" 51 cplgtdirs 55 current=`cat $LOGTALKUSER/VERSION.txt | sed 's/\.//g'` 56 if [ $current -lt 2313 ]; then 57 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 58 echo "Creating an up-to-date Logtalk user directory..." 59 cplgtdirs 60 fi 52 61 fi 53 el if ! [ -d "$LOGTALKUSER" ]; then62 else 54 63 echo "Cannot find \$LOGTALKUSER directory! Creating a new Logtalk user directory" 55 64 echo "by running the \"cplgtdirs\" shell script:" -
trunk/integration/ciaolgt.sh
r4036 r4049 1 #/bin/ sh1 #/bin/bash 2 2 3 3 ## ================================================================ … … 43 43 echo "to your Logtalk user directory!" 44 44 echo "Trying the default location for the Logtalk user directory..." 45 echo 45 46 export LOGTALKUSER=$HOME/logtalk 46 if [ -d "$LOGTALKUSER" ]; then 47 echo "... using Logtalk user directory found at $LOGTALKUSER" 47 fi 48 49 if [ -d "$LOGTALKUSER" ]; then 50 if ! [ -a "$LOGTALKUSER/VERSION.txt" ]; then 51 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 52 echo "Creating an up-to-date Logtalk user directory..." 53 cplgtdirs 48 54 else 49 echo "... Logtalk user directory not found at default location. Creating a" 50 echo "new Logtalk user directory by running the \"cplgtdirs\" shell script:" 51 cplgtdirs 55 current=`cat $LOGTALKUSER/VERSION.txt | sed 's/\.//g'` 56 if [ $current -lt 2313 ]; then 57 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 58 echo "Creating an up-to-date Logtalk user directory..." 59 cplgtdirs 60 fi 52 61 fi 53 el if ! [ -d "$LOGTALKUSER" ]; then62 else 54 63 echo "Cannot find \$LOGTALKUSER directory! Creating a new Logtalk user directory" 55 64 echo "by running the \"cplgtdirs\" shell script:" -
trunk/integration/cxlgt.sh
r4036 r4049 1 #/bin/ sh1 #/bin/bash 2 2 3 3 ## ================================================================ … … 37 37 exit 1 38 38 fi 39 40 39 export LOGTALKHOME 41 40 … … 44 43 echo "to your Logtalk user directory!" 45 44 echo "Trying the default location for the Logtalk user directory..." 45 echo 46 46 export LOGTALKUSER=$HOME/logtalk 47 if [ -d "$LOGTALKUSER" ]; then 48 echo "... using Logtalk user directory found at $LOGTALKUSER" 47 fi 48 49 if [ -d "$LOGTALKUSER" ]; then 50 if ! [ -a "$LOGTALKUSER/VERSION.txt" ]; then 51 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 52 echo "Creating an up-to-date Logtalk user directory..." 53 cplgtdirs 49 54 else 50 echo "... Logtalk user directory not found at default location. Creating a" 51 echo "new Logtalk user directory by running the \"cplgtdirs\" shell script:" 52 cplgtdirs 55 current=`cat $LOGTALKUSER/VERSION.txt | sed 's/\.//g'` 56 if [ $current -lt 2313 ]; then 57 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 58 echo "Creating an up-to-date Logtalk user directory..." 59 cplgtdirs 60 fi 53 61 fi 54 el if ! [ -d "$LOGTALKUSER" ]; then62 else 55 63 echo "Cannot find \$LOGTALKUSER directory! Creating a new Logtalk user directory" 56 64 echo "by running the \"cplgtdirs\" shell script:" -
trunk/integration/eclipselgt.sh
r4036 r4049 1 #/bin/ sh1 #/bin/bash 2 2 3 3 ## ================================================================ … … 43 43 echo "to your Logtalk user directory!" 44 44 echo "Trying the default location for the Logtalk user directory..." 45 echo 45 46 export LOGTALKUSER=$HOME/logtalk 46 if [ -d "$LOGTALKUSER" ]; then 47 echo "... using Logtalk user directory found at $LOGTALKUSER" 47 fi 48 49 if [ -d "$LOGTALKUSER" ]; then 50 if ! [ -a "$LOGTALKUSER/VERSION.txt" ]; then 51 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 52 echo "Creating an up-to-date Logtalk user directory..." 53 cplgtdirs 48 54 else 49 echo "... Logtalk user directory not found at default location. Creating a" 50 echo "new Logtalk user directory by running the \"cplgtdirs\" shell script:" 51 cplgtdirs 55 current=`cat $LOGTALKUSER/VERSION.txt | sed 's/\.//g'` 56 if [ $current -lt 2313 ]; then 57 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 58 echo "Creating an up-to-date Logtalk user directory..." 59 cplgtdirs 60 fi 52 61 fi 53 el if ! [ -d "$LOGTALKUSER" ]; then62 else 54 63 echo "Cannot find \$LOGTALKUSER directory! Creating a new Logtalk user directory" 55 64 echo "by running the \"cplgtdirs\" shell script:" -
trunk/integration/gplgt.sh
r4036 r4049 1 #/bin/ sh1 #/bin/bash 2 2 3 3 ## ================================================================ … … 43 43 echo "to your Logtalk user directory!" 44 44 echo "Trying the default location for the Logtalk user directory..." 45 echo 45 46 export LOGTALKUSER=$HOME/logtalk 46 if [ -d "$LOGTALKUSER" ]; then 47 echo "... using Logtalk user directory found at $LOGTALKUSER" 47 fi 48 49 if [ -d "$LOGTALKUSER" ]; then 50 if ! [ -a "$LOGTALKUSER/VERSION.txt" ]; then 51 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 52 echo "Creating an up-to-date Logtalk user directory..." 53 cplgtdirs 48 54 else 49 echo "... Logtalk user directory not found at default location. Creating a" 50 echo "new Logtalk user directory by running the \"cplgtdirs\" shell script:" 51 cplgtdirs 55 current=`cat $LOGTALKUSER/VERSION.txt | sed 's/\.//g'` 56 if [ $current -lt 2313 ]; then 57 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 58 echo "Creating an up-to-date Logtalk user directory..." 59 cplgtdirs 60 fi 52 61 fi 53 el if ! [ -d "$LOGTALKUSER" ]; then62 else 54 63 echo "Cannot find \$LOGTALKUSER directory! Creating a new Logtalk user directory" 55 64 echo "by running the \"cplgtdirs\" shell script:" -
trunk/integration/NOTES.txt
r4036 r4049 49 49 The environment variables LOGTALKHOME and LOGTALKUSER should be defined 50 50 in order to run the integration scripts (see the "INSTALL.txt" file for 51 details on setting the variables). 51 details on setting the variables). When the scripts detect an outdated 52 Logtalk user directory, they create a new one by running the "cplgtdirs.sh" 53 script (a backup is automatically made of the old directory). 52 54 53 55 Note that the integration scripts and shortcuts may fail if you use non- -
trunk/integration/plclgt.sh
r4036 r4049 1 #/bin/ sh1 #/bin/bash 2 2 3 3 ## ================================================================ … … 43 43 echo "to your Logtalk user directory!" 44 44 echo "Trying the default location for the Logtalk user directory..." 45 echo 45 46 export LOGTALKUSER=$HOME/logtalk 46 if [ -d "$LOGTALKUSER" ]; then 47 echo "... using Logtalk user directory found at $LOGTALKUSER" 47 fi 48 49 if [ -d "$LOGTALKUSER" ]; then 50 if ! [ -a "$LOGTALKUSER/VERSION.txt" ]; then 51 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 52 echo "Creating an up-to-date Logtalk user directory..." 53 cplgtdirs 48 54 else 49 echo "... Logtalk user directory not found at default location. Creating a" 50 echo "new Logtalk user directory by running the \"cplgtdirs\" shell script:" 51 cplgtdirs 55 current=`cat $LOGTALKUSER/VERSION.txt | sed 's/\.//g'` 56 if [ $current -lt 2313 ]; then 57 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 58 echo "Creating an up-to-date Logtalk user directory..." 59 cplgtdirs 60 fi 52 61 fi 53 el if ! [ -d "$LOGTALKUSER" ]; then62 else 54 63 echo "Cannot find \$LOGTALKUSER directory! Creating a new Logtalk user directory" 55 64 echo "by running the \"cplgtdirs\" shell script:" -
trunk/integration/qplgt.sh
r4036 r4049 1 #/bin/ sh1 #/bin/bash 2 2 3 3 ## ================================================================ … … 43 43 echo "to your Logtalk user directory!" 44 44 echo "Trying the default location for the Logtalk user directory..." 45 echo 45 46 export LOGTALKUSER=$HOME/logtalk 46 if [ -d "$LOGTALKUSER" ]; then 47 echo "... using Logtalk user directory found at $LOGTALKUSER" 47 fi 48 49 if [ -d "$LOGTALKUSER" ]; then 50 if ! [ -a "$LOGTALKUSER/VERSION.txt" ]; then 51 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 52 echo "Creating an up-to-date Logtalk user directory..." 53 cplgtdirs 48 54 else 49 echo "... Logtalk user directory not found at default location. Creating a" 50 echo "new Logtalk user directory by running the \"cplgtdirs\" shell script:" 51 cplgtdirs 55 current=`cat $LOGTALKUSER/VERSION.txt | sed 's/\.//g'` 56 if [ $current -lt 2313 ]; then 57 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 58 echo "Creating an up-to-date Logtalk user directory..." 59 cplgtdirs 60 fi 52 61 fi 53 el if ! [ -d "$LOGTALKUSER" ]; then62 else 54 63 echo "Cannot find \$LOGTALKUSER directory! Creating a new Logtalk user directory" 55 64 echo "by running the \"cplgtdirs\" shell script:" -
trunk/integration/quintuslgt.sh
r4040 r4049 1 #/bin/ sh1 #/bin/bash 2 2 3 3 ## ================================================================ … … 43 43 echo "to your Logtalk user directory!" 44 44 echo "Trying the default location for the Logtalk user directory..." 45 echo 45 46 export LOGTALKUSER=$HOME/logtalk 46 if [ -d "$LOGTALKUSER" ]; then 47 echo "... using Logtalk user directory found at $LOGTALKUSER" 47 fi 48 49 if [ -d "$LOGTALKUSER" ]; then 50 if ! [ -a "$LOGTALKUSER/VERSION.txt" ]; then 51 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 52 echo "Creating an up-to-date Logtalk user directory..." 53 cplgtdirs 48 54 else 49 echo "... Logtalk user directory not found at default location. Creating a" 50 echo "new Logtalk user directory by running the \"cplgtdirs\" shell script:" 51 cplgtdirs 55 current=`cat $LOGTALKUSER/VERSION.txt | sed 's/\.//g'` 56 if [ $current -lt 2313 ]; then 57 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 58 echo "Creating an up-to-date Logtalk user directory..." 59 cplgtdirs 60 fi 52 61 fi 53 el if ! [ -d "$LOGTALKUSER" ]; then62 else 54 63 echo "Cannot find \$LOGTALKUSER directory! Creating a new Logtalk user directory" 55 64 echo "by running the \"cplgtdirs\" shell script:" -
trunk/integration/sicstuslgt.sh
r4036 r4049 1 #/bin/ sh1 #/bin/bash 2 2 3 3 ## ================================================================ … … 43 43 echo "to your Logtalk user directory!" 44 44 echo "Trying the default location for the Logtalk user directory..." 45 echo 45 46 export LOGTALKUSER=$HOME/logtalk 46 if [ -d "$LOGTALKUSER" ]; then 47 echo "... using Logtalk user directory found at $LOGTALKUSER" 47 fi 48 49 if [ -d "$LOGTALKUSER" ]; then 50 if ! [ -a "$LOGTALKUSER/VERSION.txt" ]; then 51 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 52 echo "Creating an up-to-date Logtalk user directory..." 53 cplgtdirs 48 54 else 49 echo "... Logtalk user directory not found at default location. Creating a" 50 echo "new Logtalk user directory by running the \"cplgtdirs\" shell script:" 51 cplgtdirs 55 current=`cat $LOGTALKUSER/VERSION.txt | sed 's/\.//g'` 56 if [ $current -lt 2313 ]; then 57 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 58 echo "Creating an up-to-date Logtalk user directory..." 59 cplgtdirs 60 fi 52 61 fi 53 el if ! [ -d "$LOGTALKUSER" ]; then62 else 54 63 echo "Cannot find \$LOGTALKUSER directory! Creating a new Logtalk user directory" 55 64 echo "by running the \"cplgtdirs\" shell script:" -
trunk/integration/swilgt.sh
r4036 r4049 1 #/bin/ sh1 #/bin/bash 2 2 3 3 ## ================================================================ … … 43 43 echo "to your Logtalk user directory!" 44 44 echo "Trying the default location for the Logtalk user directory..." 45 echo 45 46 export LOGTALKUSER=$HOME/logtalk 46 if [ -d "$LOGTALKUSER" ]; then 47 echo "... using Logtalk user directory found at $LOGTALKUSER" 47 fi 48 49 if [ -d "$LOGTALKUSER" ]; then 50 if ! [ -a "$LOGTALKUSER/VERSION.txt" ]; then 51 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 52 echo "Creating an up-to-date Logtalk user directory..." 53 cplgtdirs 48 54 else 49 echo "... Logtalk user directory not found at default location. Creating a" 50 echo "new Logtalk user directory by running the \"cplgtdirs\" shell script:" 51 cplgtdirs 55 current=`cat $LOGTALKUSER/VERSION.txt | sed 's/\.//g'` 56 if [ $current -lt 2313 ]; then 57 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 58 echo "Creating an up-to-date Logtalk user directory..." 59 cplgtdirs 60 fi 52 61 fi 53 el if ! [ -d "$LOGTALKUSER" ]; then62 else 54 63 echo "Cannot find \$LOGTALKUSER directory! Creating a new Logtalk user directory" 55 64 echo "by running the \"cplgtdirs\" shell script:" -
trunk/integration/xsblgt.sh
r4036 r4049 1 #/bin/ sh1 #/bin/bash 2 2 3 3 ## ================================================================ … … 43 43 echo "to your Logtalk user directory!" 44 44 echo "Trying the default location for the Logtalk user directory..." 45 echo 45 46 export LOGTALKUSER=$HOME/logtalk 46 if [ -d "$LOGTALKUSER" ]; then 47 echo "... using Logtalk user directory found at $LOGTALKUSER" 47 fi 48 49 if [ -d "$LOGTALKUSER" ]; then 50 if ! [ -a "$LOGTALKUSER/VERSION.txt" ]; then 51 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 52 echo "Creating an up-to-date Logtalk user directory..." 53 cplgtdirs 48 54 else 49 echo "... Logtalk user directory not found at default location. Creating a" 50 echo "new Logtalk user directory by running the \"cplgtdirs\" shell script:" 51 cplgtdirs 55 current=`cat $LOGTALKUSER/VERSION.txt | sed 's/\.//g'` 56 if [ $current -lt 2313 ]; then 57 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 58 echo "Creating an up-to-date Logtalk user directory..." 59 cplgtdirs 60 fi 52 61 fi 53 el if ! [ -d "$LOGTALKUSER" ]; then62 else 54 63 echo "Cannot find \$LOGTALKUSER directory! Creating a new Logtalk user directory" 55 64 echo "by running the \"cplgtdirs\" shell script:" -
trunk/integration/xsbmtlgt.sh
r4036 r4049 1 #/bin/ sh1 #/bin/bash 2 2 3 3 ## ================================================================ … … 43 43 echo "to your Logtalk user directory!" 44 44 echo "Trying the default location for the Logtalk user directory..." 45 echo 45 46 export LOGTALKUSER=$HOME/logtalk 46 if [ -d "$LOGTALKUSER" ]; then 47 echo "... using Logtalk user directory found at $LOGTALKUSER" 47 fi 48 49 if [ -d "$LOGTALKUSER" ]; then 50 if ! [ -a "$LOGTALKUSER/VERSION.txt" ]; then 51 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 52 echo "Creating an up-to-date Logtalk user directory..." 53 cplgtdirs 48 54 else 49 echo "... Logtalk user directory not found at default location. Creating a" 50 echo "new Logtalk user directory by running the \"cplgtdirs\" shell script:" 51 cplgtdirs 55 current=`cat $LOGTALKUSER/VERSION.txt | sed 's/\.//g'` 56 if [ $current -lt 2313 ]; then 57 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 58 echo "Creating an up-to-date Logtalk user directory..." 59 cplgtdirs 60 fi 52 61 fi 53 el if ! [ -d "$LOGTALKUSER" ]; then62 else 54 63 echo "Cannot find \$LOGTALKUSER directory! Creating a new Logtalk user directory" 55 64 echo "by running the \"cplgtdirs\" shell script:" -
trunk/integration/yaplgt.sh
r4036 r4049 1 #/bin/ sh1 #/bin/bash 2 2 3 3 ## ================================================================ … … 43 43 echo "to your Logtalk user directory!" 44 44 echo "Trying the default location for the Logtalk user directory..." 45 echo 45 46 export LOGTALKUSER=$HOME/logtalk 46 if [ -d "$LOGTALKUSER" ]; then 47 echo "... using Logtalk user directory found at $LOGTALKUSER" 47 fi 48 49 if [ -d "$LOGTALKUSER" ]; then 50 if ! [ -a "$LOGTALKUSER/VERSION.txt" ]; then 51 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 52 echo "Creating an up-to-date Logtalk user directory..." 53 cplgtdirs 48 54 else 49 echo "... Logtalk user directory not found at default location. Creating a" 50 echo "new Logtalk user directory by running the \"cplgtdirs\" shell script:" 51 cplgtdirs 55 current=`cat $LOGTALKUSER/VERSION.txt | sed 's/\.//g'` 56 if [ $current -lt 2313 ]; then 57 echo "Logtalk user directory at $LOGTALKUSER is outdated!" 58 echo "Creating an up-to-date Logtalk user directory..." 59 cplgtdirs 60 fi 52 61 fi 53 el if ! [ -d "$LOGTALKUSER" ]; then62 else 54 63 echo "Cannot find \$LOGTALKUSER directory! Creating a new Logtalk user directory" 55 64 echo "by running the \"cplgtdirs\" shell script:"
