my ($script, $format) = lookup_script($fname);
open SCRIPT, "< $script" or die "Can't open Matita script \"$script\"\n";
my @lines = <SCRIPT>;
my ($script, $format) = lookup_script($fname);
open SCRIPT, "< $script" or die "Can't open Matita script \"$script\"\n";
my @lines = <SCRIPT>;