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