Admin/Mercurial/isabelle-style-1.4.3--1.8.2.diff
author haftmann
Fri, 14 Jun 2019 08:34:27 +0000
changeset 70335 9bd8c16b6627
parent 42432 e1657125da76
permissions -rw-r--r--
using (*)-syntax for partially applied infix is fine, contrary to ancient op-syntax
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42432
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
     1
diff -Naur gitweb/changelogentry.tmpl isabelle/changelogentry.tmpl
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
     2
--- gitweb/changelogentry.tmpl	2011-04-20 12:27:29.000000000 +0200
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
     3
+++ isabelle/changelogentry.tmpl	2011-04-20 12:32:48.000000000 +0200
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
     4
@@ -1,14 +1,12 @@
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
     5
 <div>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
     6
-<a class="title" href="{url}rev/{node|short}{sessionvars%urlparameter}"><span class="age">{date|age}</span>{desc|strip|firstline|escape|nonempty}<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
     7
-</div>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
     8
-<div class="title_text">
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
     9
-<div class="log_link">
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    10
-<a href="{url}rev/{node|short}{sessionvars%urlparameter}">changeset</a><br/>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    11
-</div>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    12
-<i>{author|obfuscate} [{date|rfc822date}] rev {rev}</i><br/>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    13
+<a class="title" href="{url}rev/{node|short}{sessionvars%urlparameter}"><span class="age">{date|age}</span>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    14
+{author|obfuscate} [{date|rfc822date}] rev {rev}<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    15
 </div>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    16
 <div class="log_body">
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    17
 {desc|strip|escape|addbreaks|nonempty}
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    18
 <br/>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    19
+<div class="files">
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    20
+{files}
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    21
+</div>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    22
 <br/>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    23
 </div>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    24
diff -Naur gitweb/map isabelle/map
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    25
--- gitweb/map	2011-04-20 12:27:29.000000000 +0200
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    26
+++ isabelle/map	2011-04-20 12:32:48.000000000 +0200
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    27
@@ -78,7 +78,7 @@
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    28
   <tr style="font-family:monospace" class="parity{parity}">
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    29
     <td class="linenr" style="text-align: right;">
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    30
       <a href="{url}annotate/{node|short}/{file|urlescape}{sessionvars%urlparameter}#l{targetline}"
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    31
-         title="{node|short}: {desc|escape|firstline}">{author|user}@{rev}</a>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    32
+         title="{node|short}: {desc|escape}">{author|user}@{rev}</a>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    33
     </td>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    34
     <td><pre><a class="linenr" href="#{lineid}" id="{lineid}">{linenumber}</a></pre></td>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    35
     <td><pre>{line|escape}</pre></td>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    36
@@ -206,9 +206,10 @@
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    37
   <tr class="parity{parity}">
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    38
     <td class="age"><i>{date|age}</i></td>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    39
     <td><i>{author|person}</i></td>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    40
+    <td><i>{date|shortdate}</i></td>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    41
     <td>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    42
       <a class="list" href="{url}rev/{node|short}{sessionvars%urlparameter}">
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    43
-        <b>{desc|strip|firstline|escape|nonempty}</b>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    44
+        <b>{desc|strip|escape|nonempty}</b>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    45
         <span class="logtags">{inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    46
       </a>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    47
     </td>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    48
@@ -220,9 +221,11 @@
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    49
 filelogentry = '
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    50
   <tr class="parity{parity}">
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    51
     <td class="age"><i>{date|age}</i></td>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    52
+    <td><i>{author|person}</i></td>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    53
+    <td><i>{date|shortdate}</i></td>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    54
     <td>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    55
       <a class="list" href="{url}rev/{node|short}{sessionvars%urlparameter}">
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    56
-        <b>{desc|strip|firstline|escape|nonempty}</b>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    57
+        <b>{desc|strip|escape|nonempty}</b>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    58
       </a>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    59
     </td>
e1657125da76 added template diff against newer mercurials, where the 'ago' duplication has been fixed
krauss
parents:
diff changeset
    60
     <td class="link">