From: bangerth <bangerth@0785d39b-7218-0410-832d-ea1e28bc413d>
Date: Wed, 2 Jun 2010 16:23:31 +0000 (+0000)
Subject: Work around a problem in doxygen 1.6.3.
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=9f4f487cf7c678cce44188cc62891f0c6c54de1b;p=dealii-svn.git

Work around a problem in doxygen 1.6.3.


git-svn-id: https://svn.dealii.org/trunk@21144 0785d39b-7218-0410-832d-ea1e28bc413d
---

diff --git a/deal.II/common/scripts/validate-xrefs.pl b/deal.II/common/scripts/validate-xrefs.pl
index 8b66c9704d..2913819be6 100644
--- a/deal.II/common/scripts/validate-xrefs.pl
+++ b/deal.II/common/scripts/validate-xrefs.pl
@@ -59,7 +59,8 @@ foreach $filename (@ARGV)
 	        $found = 0;
 	        while ( <IN2> ) {
 		    while ( /<a[^>]* (name=|class=\"anchor\" id=)\"?(.*?)[\s\"]/gi ) {
-		        if ( $2 eq $internal_ref) {
+		        if ( $2 eq $internal_ref)
+			{
 			    print "                    found.\n" if $debug;
 			    $found = 1;
 			    last;
@@ -68,7 +69,10 @@ foreach $filename (@ARGV)
 		}
 
 		die "---Internal reference `$internal_ref' not found in file $filename\n This line is: $this_line.\n"
-		    unless $found;
+		    unless $found
+                            # work around a bug in doxygen 1.6.3:
+			    #   https://bugzilla.gnome.org/show_bug.cgi?id=620372
+                            || ($internal_ref =~ /^index_[:_~]/) ;
 		next;
 	    }
 	    elsif ( $link =~ /^(.*?)#(.*)/ )
@@ -88,7 +92,8 @@ foreach $filename (@ARGV)
 		$found = 0;
 		while ( <IN2> ) {
 		    while ( /<a[^>]* (name=|class=\"anchor\" id=)\"?(.*?)[\s\"]/gi ) {
-			if ( $2 eq $external_ref) {
+			if ( $2 eq $external_ref)
+			{
 			    print "                    found.\n" if $debug;
 			    $found = 1;
 			    last;
@@ -97,7 +102,10 @@ foreach $filename (@ARGV)
 		}
 
 		die "---External reference `$external_file#$external_ref' not found in file $filename\n This line is: $this_line.\n"
-		    unless $found;
+		    unless $found
+                            # work around a bug in doxygen 1.6.3:
+			    #   https://bugzilla.gnome.org/show_bug.cgi?id=620372
+                            || ($external_ref =~ /^index_[:_~]/) ;
 		next;
 	    }
 	    else {