Admin/Mercurial/isabelle-style.diff

temporarily allow useless encoding of helper facts (e.g. fequal_def) instead of throwing exception

diff -r gitweb/changelogentry.tmpl isabelle/changelogentry.tmpl
2,8c2,3
< <a class="title" href="{url}rev/{node|short}{sessionvars%urlparameter}"><span class="age">{date|age} ago</span>{desc|strip|firstline|escape|nonempty}<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
< </div>
< <div class="title_text">
< <div class="log_link">
< <a href="{url}rev/{node|short}{sessionvars%urlparameter}">changeset</a><br/>
< </div>
< <i>{author|obfuscate} [{date|rfc822date}] rev {rev}</i><br/>
---
> <a class="title" href="{url}rev/{node|short}{sessionvars%urlparameter}"><span class="age">{date|age}</span>
> {author|obfuscate} [{date|rfc822date}] rev {rev}<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
12a8,10
> <div class="files">
> {files}
> </div>
diff -r gitweb/changeset.tmpl isabelle/changeset.tmpl
32c32
< <tr><td></td><td>{date|date} ({date|age} ago)</td></tr>
---
> <tr><td></td><td>{date|date} ({date|age})</td></tr>
diff -r gitweb/fileannotate.tmpl isabelle/fileannotate.tmpl
39c39
<  <td>{date|date} ({date|age} ago)</td></tr>
---
>  <td>{date|date} ({date|age})</td></tr>
diff -r gitweb/filerevision.tmpl isabelle/filerevision.tmpl
39c39
<  <td>{date|date} ({date|age} ago)</td></tr>
---
>  <td>{date|date} ({date|age})</td></tr>
diff -r gitweb/graph.tmpl isabelle/graph.tmpl
66c66
< revlink += '<span class="info">_DATE ago, by _USER</span></li>';
---
> revlink += '<span class="info">_DATE, by _USER</span></li>';
diff -r gitweb/map isabelle/map
81c81
<          title="{node|short}: {desc|escape|firstline}">{author|user}@{rev}</a>
---
>          title="{node|short}: {desc|escape}">{author|user}@{rev}</a>
153c153
<     <td class="age"><i>{date|age} ago</i></td>
---
>     <td class="age"><i>{date|age}</i></td>
164c164
<     <td class="age"><i>{date|age} ago</i></td>
---
>     <td class="age"><i>{date|age}</i></td>
207c207
<     <td class="age"><i>{date|age} ago</i></td>
---
>     <td class="age"><i>{date|age}</i></td>
208a209
>     <td><i>{date|shortdate}</i></td>
211c212
<         <b>{desc|strip|firstline|escape|nonempty}</b>
---
>         <b>{desc|strip|escape|nonempty}</b>
222c223,225
<     <td class="age"><i>{date|age} ago</i></td>
---
>     <td class="age"><i>{date|age}</i></td>
>     <td><i>{author|person}</i></td>
>     <td><i>{date|shortdate}</i></td>
225c228
<         <b>{desc|strip|firstline|escape|nonempty}</b>
---
>         <b>{desc|strip|escape|nonempty}</b>
241c244
<     <td class="age">{lastchange|age} ago</td>
---
>     <td class="age">{lastchange|age}</td>