src/Doc/ROOT
changeset 78657 0aa741c67086
parent 76649 9a6cb5ecc183
equal deleted inserted replaced
78642:4f2215cfc3e0 78657:0aa741c67086
   215     "style.sty"
   215     "style.sty"
   216   document_files
   216   document_files
   217     "auto-tools.png"
   217     "auto-tools.png"
   218     "bibtex-mode.png"
   218     "bibtex-mode.png"
   219     "cite-completion.png"
   219     "cite-completion.png"
       
   220     "document-panel.png"
   220     "isabelle-jedit.png"
   221     "isabelle-jedit.png"
   221     "markdown-document.png"
   222     "markdown-document.png"
   222     "ml-debugger.png"
   223     "ml-debugger.png"
   223     "output-and-state.png"
   224     "output-and-state.png"
   224     "output-including-state.png"
   225     "output-including-state.png"