diff --git a/doc/fixnavi.pl b/doc/fixnavi.pl
index d0350b76357..bf6acaa3839 100755
--- a/doc/fixnavi.pl
+++ b/doc/fixnavi.pl
@@ -27,7 +27,7 @@ while (<FILE>) {
     } else {
         if (/^\h*\\endlist/) {
             $intoc--;
-        } elsif (/^\h*\\o\h+\\l{(.*)}$/) {
+        } elsif (/^\h*\\o\h+\\l\h*{(.*)}$/) {
             push @toc, $1;
         }
     }