Imported Upstream version 4.7.2

install/ui/util/change-profile.sh

@@ -18,6 +18,7 @@
 #
 #  You should have received a copy of the GNU General Public License
 #  along with this program.  If not, see <http://www.gnu.org/licenses/>.
+set -o errexit
 
 DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
 RDIR=$DIR/../release
@@ -139,4 +140,4 @@ pushd $DIR/../js
         git update-index --no-assume-unchanged ./dojo
         git update-index --no-assume-unchanged ./freeipa
     fi
-popd
+popd