/** Returns the current freefont, encoded as a std::string to be passed to the
* frontends.
*/
std::string const freefont2string();
/** Returns the current freefont, encoded as a std::string to be passed to the
* frontends.
*/
std::string const freefont2string();