// -*- coding: utf-8 -*-
var str = "𝔘𝔫𝔦𝔠𝔬𝔡𝔢";
function f() { return 42; }