/* one parameter: version of deprecation (optional) */
/* prepend version with HTML, CSS, JS or Gecko for those techs */
/* for backwards compatibility unprefixed is Gecko, please avoid this */

var str = "";

if ($0) {
  if (string.isdigit($0)) {
    let str = "gecko" .. $0;
  }
  else {
    let str = $0
  }
}

template.deprecatedGeneric("header",str);