cp  readme_eclipse.html readme_eclipse_old.html
sed -i -e 's/4\.24/4\.25/g'  readme_eclipse.html
sed -i -e 's/4_24/4_25/g' readme_eclipse.html
sed -i -e 's/4\.23/4\.24/g' readme_eclipse.html