From b0fbc80495b45939321358981fa080b89be65065 Mon Sep 17 00:00:00 2001
From: "Achim D. Brucker" <adbrucker@0x5f.org>
Date: Sun, 7 Apr 2019 17:41:41 +0100
Subject: [PATCH] Excluded example of dangling reference from LaTex generation.

---
 examples/cenelec/mini_odo/mini_odo.thy | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/examples/cenelec/mini_odo/mini_odo.thy b/examples/cenelec/mini_odo/mini_odo.thy
index 12dd136..d442de8 100644
--- a/examples/cenelec/mini_odo/mini_odo.thy
+++ b/examples/cenelec/mini_odo/mini_odo.thy
@@ -70,9 +70,11 @@ section*[h::example]\<open> Some global inspection commands for the status of do
 
 
 section*[i::example]\<open> Text Antiquotation Infrastructure ... \<close>  
-                  
+                 
+(*<*)
 text\<open> @{docitem \<open>lalala\<close>}   -- produces warning. \<close>  
 text\<open> @{docitem (unchecked) \<open>lalala\<close>} -- produces no warning. \<close>  
+(*>*)
 
 text\<open> @{docitem \<open>ass122\<close>} -- global reference to a text-item in another file. \<close>