NEWS
changeset 81117 0c898f7d9b15
parent 81116 0fb1e2dd4122
child 81121 7cacedbddba7
equal deleted inserted replaced
81116:0fb1e2dd4122 81117:0c898f7d9b15
   136 LaTeX. Rare INCOMPATIBILITY for ambitious document antiquotations that
   136 LaTeX. Rare INCOMPATIBILITY for ambitious document antiquotations that
   137 generate Latex source on their own account, instead of using regular
   137 generate Latex source on their own account, instead of using regular
   138 Pretty.T interfaces (that are based on Latex.output_ops internally).
   138 Pretty.T interfaces (that are based on Latex.output_ops internally).
   139 Note that basic Markup.markup cannot be used for Latex output: proper
   139 Note that basic Markup.markup cannot be used for Latex output: proper
   140 Pretty.T operations are required (e.g. Pretty.mark_str).
   140 Pretty.T operations are required (e.g. Pretty.mark_str).
       
   141 
       
   142 * Antiquotation \<^bundle>\<open>name\<close> inlines a formally checked bundle name.
   141 
   143 
   142 
   144 
   143 *** System ***
   145 *** System ***
   144 
   146 
   145 * The Build_Manager module has replaced previous glue-code for Jenkins
   147 * The Build_Manager module has replaced previous glue-code for Jenkins