booking change request html editor error

If I want to request a booking change for a booked resource, I get a coding error,
saying "can_use_html_editor" not longer supported.

The issue can be resolved by the following patch:

diff -u request_vacate.php.orig request_vacate.php
— request_vacate.php.orig 2016-02-21 12:57:41.556804703 +0100
+++ request_vacate.php 2016-02-21 12:17:28.005831903 +0100
@@ -43,7 +43,7 @@
<div id="request_vacate">
<input type="hidden" name="id" value="'.$booking->userid.'" />
<input type="hidden" name="sesskey" value="'.sesskey().'" />';

• $usehtmleditor = (can_use_html_editor());
  + $usehtmleditor = true;
  if ($usehtmleditor) {
  print_textarea($usehtmleditor, 15, 350, 0, 0, 'message', get_string('requestvacatemessage_html','block_mrbs',$messagelang));
  echo '<input type="hidden" name="format" value="'.FORMAT_HTML.'" />';