Browse Source

Correct bug in version_set script

Leo 9 years ago
parent
commit
70db3611fe
1 changed files with 1 additions and 1 deletions
  1. 1 1
      version_set.sh

+ 1 - 1
version_set.sh

@@ -11,7 +11,7 @@ new_version=$1
 
 
 # Print what will be done
-echo "Put" $new_version "instead of" $new_version
+echo "Put" $new_version "instead of" $current_version
 
 # Replace in the 4 files : VERSION, _oasis, src/oclaunch.ml, opam
 echo $new_version > VERSION