Project

General

Profile

Revision 32e6c218

View differences:

svn_version.sh
2 2

  
3 3
version=`svn info | awk -v ver="UNKNOWN" -F ":" '/R?vision/ { ver=$2 } END { print ver }' | tr -d " "`
4 4

  
5
if [ $version = 'UNKNOWN' ] ; then
6
  version=$(git rev-parse HEAD)
7
fi
8

  
9
if [ -z $version ] ; then
10
  version=UNKNOWN
11
fi 
12

  
5 13
filename=version.ml
6 14
prefix=$1
7 15

  
......
15 23
echo "" >> src/${filename}
16 24
echo "let prefix = \"${prefix}\"" >> src/${filename}
17 25
echo "installation path prefix: ${prefix}"
18
echo "... done"
26
echo "... done"

Also available in: Unified diff