diff --git a/doc/eigen_navtree_hacks.js b/doc/eigen_navtree_hacks.js index f36b332ec..605fb5f10 100644 --- a/doc/eigen_navtree_hacks.js +++ b/doc/eigen_navtree_hacks.js @@ -360,8 +360,8 @@ $(document).ready(function() { (function (){ // wait until the first "selected" element has been created try { - - // this line will triger an exception if there is no #selected element, i.e., before the tree structure is complete. + // this line will triger an exception if there is no #selected element, i.e., before the tree structure is + // complete. document.getElementById("selected").className = "item selected"; // ok, the default tree has been created, we can keep going...