equal
deleted
inserted
replaced
47 ^doc-src/.*\.ind |
47 ^doc-src/.*\.ind |
48 ^doc-src/.*\.lof |
48 ^doc-src/.*\.lof |
49 ^doc-src/.*\.log |
49 ^doc-src/.*\.log |
50 ^doc-src/.*\.nav |
50 ^doc-src/.*\.nav |
51 ^doc-src/.*\.out |
51 ^doc-src/.*\.out |
52 ^doc-src/.*\.toc |
|
53 ^src/Tools/jEdit/dist/ |
|
54 |
|
55 # from Isabelle2002, 2011 |
|
56 |
|
57 ^doc/.* |
|
58 ^doc-src/.*\.brf |
|
59 ^doc-src/.*\.lot |
|
60 ^doc-src/.*\.lot |
|
61 ^doc-src/.*\.nav |
|
62 ^doc-src/.*\.pdf |
|
63 ^doc-src/.*\.rai |
52 ^doc-src/.*\.rai |
64 ^doc-src/.*\.rao |
53 ^doc-src/.*\.rao |
65 ^doc-src/.*\.snm |
54 ^doc-src/.*\.snm |
66 ^doc-src/.*\.synctex |
55 ^doc-src/.*\.synctex |
67 ^doc-src/.*\.tex.backup |
56 ^doc-src/.*\.tex.backup |