/usr/lib/petscdir/3.7.5/x86_64-linux-gnu-complex/bin/urlget is in libpetsc-complex-3.7.5-dev 3.7.5+dfsg1-4+b1.
This file is owned by root:root, with mode 0o755.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 | #! /bin/sh
#
# Locate urlget.py
#
if [ -x urlget.py ]; then
URLGET=./urlget.py
fi
if [ "$URLGET" = "" ]; then
for i in $PATH
do
if [ -x $i/urlget.py ]; then
URLGET=$i/urlget.py
break
fi
done
fi
if [ "$URLGET" = "" ]; then
if [ "$PETSC_DIR" != "" ]; then
if [ -d $PETSC_DIR ]; then
if [ ! -x $PETSC_DIR/bin/urlget.py ]; then
# echo PETSC_DIR is set but cannot locate bin/urlget.py
PETSC_DIR=""
fi
else
# echo PETSC_DIR is set but does not point to valid directory
PETSC_DIR=""
fi
else
if [ -x bin/urlget.py ]; then
PETSC_DIR=`pwd`
fi
fi
if [ "$PETSC_DIR" != "" ]; then
URLGET=$PETSC_DIR/bin/urlget.py
fi
fi
#
# Check if urlget.py works
#
if [ "$URLGET" != "" ]; then
$URLGET -v > /dev/null 2>&1
if [ $? -ne 0 ]; then
#
# Find Python
#
for i in python python1.5 python2 /usr/local/bin/python
do
$i -help > /dev/null 2>&1
if [ $? -ne 127 ]; then
PYTHON=$i
break
fi
done
if [ "$PYTHON" != "" ]; then
#
# Patch urlget.py to use correct python
#
sed -e "s?python1.4?$PYTHON?g" $URLGET > .tmp
mv -f .tmp $URLGET
chmod ugo+x $URLGET
#
# Check if urlget.py works
#
$URLGET -v > /dev/null 2>&1
if [ $? -ne 0 ]; then
# echo "Could not get python to work with urlget.py on your machine"
URLGET=""
fi
else
# echo "Could not locate python on machine"
URLGET=""
fi
fi
fi
#
#
#
if [ "$URLGET" != "" ]; then
$URLGET $*
exit
fi
#
# Try to use wget
#
# Does wget exist and seem to work?
#
wget -help > /dev/null 2>&1
if [ $? -eq 0 ]; then
if [ "$1" = "-v" ]; then
exit 0
fi
#
# Get the requested file
#
flag1=`echo $file | sed -e "s?http://[-a-zA-Z_0-9.]*.gz?yes?g"`
flag2=`echo $file | sed -e "s?ftp://[-a-zA-Z_0-9.]*.gz?yes?g"`
if [ "$flag1" = "yes" -o "$flag2" = "yes" ] ; then
wget -r $* > /dev/null 2>&1
if [ $? -ne 0 ]; then
exit 0
fi
else
cp -f $* .
fi
file=`basename $*`
#
# uncompress it if it is gziped
#
flag=`echo $file | sed -e "s/[-a-zA-Z_0-9.]*.gz/yes/g"`
if [ "$flag" = "yes" ] ; then
gunzip -f $file > /dev/null 2>&1
file=`echo $file | sed -e "s/\([-a-zA-Z_0-9.]*\).gz/\1/g"`
fi
echo $file
exit 0
fi
|