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