$output_string .= "<?xml version='1.0'?>\n";
$output_string .= "<!DOCTYPE platform SYSTEM \"simgrid.dtd\">\n";
$output_string .= "<?xml version='1.0'?>\n";
$output_string .= "<!DOCTYPE platform SYSTEM \"simgrid.dtd\">\n";
# eat the header, whatever form it has
next if ($line =~ s/<\?xml[^>]*>// && ! $line =~ /\S/); # just in case several tags are on the same line
next if ($line =~ s/<!DOCTYPE[^>]*>// && ! $line =~ /\S/);
# eat the header, whatever form it has
next if ($line =~ s/<\?xml[^>]*>// && ! $line =~ /\S/); # just in case several tags are on the same line
next if ($line =~ s/<!DOCTYPE[^>]*>// && ! $line =~ /\S/);
$fromversion = $1;
if ($fromversion == $toversion) {
warn "Input platform file version is already $fromversion. This should be a no-op.\n";
$fromversion = $1;
if ($fromversion == $toversion) {
warn "Input platform file version is already $fromversion. This should be a no-op.\n";
if ($fromversion > $toversion) {
die "Input platform file version is more recent than this script (file version: $fromversion; script version: $toversion)\n";
}
if ($fromversion > $toversion) {
die "Input platform file version is more recent than this script (file version: $fromversion; script version: $toversion)\n";
}