diff options
| author | paltherr <paltherr@epfl.ch> | 2004-01-12 15:21:45 +0000 |
|---|---|---|
| committer | paltherr <paltherr@epfl.ch> | 2004-01-12 15:21:45 +0000 |
| commit | 94d3acbf636e343e18d3c3596240054719a2f586 (patch) | |
| tree | db8864959b027c9541d8ca56218fa33027de7fec /support/scripts | |
| parent | fdfbbfd640b7076156427636dfed5ab3d622eb01 (diff) | |
| download | scala-94d3acbf636e343e18d3c3596240054719a2f586.tar.gz scala-94d3acbf636e343e18d3c3596240054719a2f586.tar.bz2 scala-94d3acbf636e343e18d3c3596240054719a2f586.zip | |
- Added website-print-xml*
Diffstat (limited to 'support/scripts')
| -rwxr-xr-x | support/scripts/website-print-xml | 11 | ||||
| -rwxr-xr-x | support/scripts/website-print-xml-distributions | 11 | ||||
| -rwxr-xr-x | support/scripts/website-print-xml-installers | 11 |
3 files changed, 33 insertions, 0 deletions
diff --git a/support/scripts/website-print-xml b/support/scripts/website-print-xml new file mode 100755 index 0000000000..502e10be3c --- /dev/null +++ b/support/scripts/website-print-xml @@ -0,0 +1,11 @@ +#!/bin/bash +########################################################-*-Shell-script-*-#### +# Website-Print-XML Command +############################################################################## +# $Id$ + +program="${0##*/}"; +source "${0%/*}/${program%%-*}.sh"; +"$program" "$@"; + +############################################################################## diff --git a/support/scripts/website-print-xml-distributions b/support/scripts/website-print-xml-distributions new file mode 100755 index 0000000000..69f22093ed --- /dev/null +++ b/support/scripts/website-print-xml-distributions @@ -0,0 +1,11 @@ +#!/bin/bash +########################################################-*-Shell-script-*-#### +# Website-Print-XML-Distributions Command +############################################################################## +# $Id$ + +program="${0##*/}"; +source "${0%/*}/${program%%-*}.sh"; +"$program" "$@"; + +############################################################################## diff --git a/support/scripts/website-print-xml-installers b/support/scripts/website-print-xml-installers new file mode 100755 index 0000000000..933688d0fc --- /dev/null +++ b/support/scripts/website-print-xml-installers @@ -0,0 +1,11 @@ +#!/bin/bash +########################################################-*-Shell-script-*-#### +# Website-Print-XML-Installers Command +############################################################################## +# $Id$ + +program="${0##*/}"; +source "${0%/*}/${program%%-*}.sh"; +"$program" "$@"; + +############################################################################## |