Brought back revision 8096.
The command used was: svn merge -r8095:8096 .
This was done since r8117 reverted accidentally both r8096 and r8097, while only r8097 had to be reverted.
Authored by: semor 2008-12-04
Parent: [r8118]
Child: [r8120]
