devops.texi: Punt empty @detailmenu.

diff --git a/src/devops/devops.texi b/src/devops/devops.texi
index ba1baefa101bd2624957816cc0ec0926ff51377c..ad3bb85138248cee2314bf0c668efd3ecf1dc205 100644 (file)
--- a/src/devops/devops.texi
+++ b/src/devops/devops.texi
@@ -69,11 +69,6 @@ Documentation License.''
 * Build System:: How so ``supported?''
 * GNU Free Documentation License::  
 * Concept Index::               
-
-@detailmenu
- --- The Detailed Node Listing ---
-
-@end detailmenu
 @end menu
 
 @node Introduction