Topic: $theme already found

File: includes/page/header.inc

Line 85 already assigns $theme = user_theme();.
Hence line 139:

    include_once($path_to_root . "/themes/".user_theme()."/renderer.php");

can become

    include_once($path_to_root . "/themes/$theme/renderer.php");

Re: $theme already found

Sure, thanks.

Re: $theme already found

HG 3212 does the job. All line endings fixed as well. Thanks Janusz for the quick turnaround.