filesystem: script 'dune' now saves user parameters on upgrade. This commit closes #2603

This commit is contained in:
Ricardo Martins 2013-12-02 11:41:20 +00:00
parent 660a2a20f0
commit 6990d3f0f8

View File

@ -14,6 +14,7 @@ maybe_upgrade()
rm -rf $dune_base/.dune-upgrade &&
mkdir $dune_base/.dune-upgrade &&
tar -x -C $dune_base/.dune-upgrade -f $dune_base/dune-*.tar.bz2 &&
cp "$dune_base/etc/"*-saved.ini "$dune_base/.dune-upgrade/"dune-*/etc 2> /dev/null &&
rm $dune_base/dune-*.tar.bz2 &&
for dir in $dune_base/.dune-upgrade/dune-*/*; do
d="$(basename "$dir")"