equal
deleted
inserted
replaced
25 src/Pure/Admin/component_e.scala \ |
25 src/Pure/Admin/component_e.scala \ |
26 src/Pure/Admin/component_easychair.scala \ |
26 src/Pure/Admin/component_easychair.scala \ |
27 src/Pure/Admin/component_eptcs.scala \ |
27 src/Pure/Admin/component_eptcs.scala \ |
28 src/Pure/Admin/component_foiltex.scala \ |
28 src/Pure/Admin/component_foiltex.scala \ |
29 src/Pure/Admin/component_fonts.scala \ |
29 src/Pure/Admin/component_fonts.scala \ |
30 src/Pure/Admin/component_go.scala \ |
|
31 src/Pure/Admin/component_hugo.scala \ |
30 src/Pure/Admin/component_hugo.scala \ |
32 src/Pure/Admin/component_javamail.scala \ |
31 src/Pure/Admin/component_javamail.scala \ |
33 src/Pure/Admin/component_jdk.scala \ |
32 src/Pure/Admin/component_jdk.scala \ |
34 src/Pure/Admin/component_jedit.scala \ |
33 src/Pure/Admin/component_jedit.scala \ |
35 src/Pure/Admin/component_jsoup.scala \ |
34 src/Pure/Admin/component_jsoup.scala \ |
210 src/Pure/Tools/docker_build.scala \ |
209 src/Pure/Tools/docker_build.scala \ |
211 src/Pure/Tools/dotnet_setup.scala \ |
210 src/Pure/Tools/dotnet_setup.scala \ |
212 src/Pure/Tools/dump.scala \ |
211 src/Pure/Tools/dump.scala \ |
213 src/Pure/Tools/flarum.scala \ |
212 src/Pure/Tools/flarum.scala \ |
214 src/Pure/Tools/fontforge.scala \ |
213 src/Pure/Tools/fontforge.scala \ |
|
214 src/Pure/Tools/go_setup.scala \ |
215 src/Pure/Tools/java_monitor.scala \ |
215 src/Pure/Tools/java_monitor.scala \ |
216 src/Pure/Tools/logo.scala \ |
216 src/Pure/Tools/logo.scala \ |
217 src/Pure/Tools/mkroot.scala \ |
217 src/Pure/Tools/mkroot.scala \ |
218 src/Pure/Tools/phabricator.scala \ |
218 src/Pure/Tools/phabricator.scala \ |
219 src/Pure/Tools/print_operation.scala \ |
219 src/Pure/Tools/print_operation.scala \ |