updated screenshot;
authorwenzelm
Mon Aug 06 15:19:39 2018 +0200 (4 months ago)
changeset 68737a8bef9ff7dc0
parent 68736 29dbf3408021
child 68738 34b8ff7cb109
updated screenshot;
src/Doc/JEdit/JEdit.thy
src/Doc/JEdit/document/bibtex-mode.png
     1.1 --- a/src/Doc/JEdit/JEdit.thy	Mon Aug 06 14:29:46 2018 +0200
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Mon Aug 06 15:19:39 2018 +0200
     1.3 @@ -1907,7 +1907,8 @@
     1.4    \begin{center}
     1.5    \includegraphics[scale=0.333]{bibtex-mode}
     1.6    \end{center}
     1.7 -  \caption{Bib{\TeX} mode with context menu and SideKick tree view}
     1.8 +  \caption{Bib{\TeX} mode with context menu, SideKick tree view, and
     1.9 +    semantic output from the \<^verbatim>\<open>bibtex\<close> tool}
    1.10    \label{fig:bibtex-mode}
    1.11    \end{figure}
    1.12  
     2.1 Binary file src/Doc/JEdit/document/bibtex-mode.png has changed