Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Admin/build/TUM.toml
author wenzelm
Wed, 15 Jan 2025 15:49:16 +0100
changeset 81826 57b0a02e2774
parent 81468 3279f71eb0f4
permissions -rw-r--r--
clarified signature: more explicit operations;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
78946
87ac093e4d1a some build cluster resources at TUM;
wenzelm
parents:
diff changeset 
     1
 
# Build cluster resources at TUM
87ac093e4d1a some build cluster resources at TUM;
wenzelm
parents:
diff changeset 
     2
 












87ac093e4d1a
some build cluster resources at TUM;



wenzelm


parents: 

diff
changeset




     3


[host.lxbroy10]








81468






3279f71eb0f4
avoid informatik.tu-muenchen.de domain: soon to be discontinued;



Fabian Huch <huch@in.tum.de>


parents: 
78946

diff
changeset




     4


hostname = "lxbroy10.in.tum.de"








78946






87ac093e4d1a
some build cluster resources at TUM;



wenzelm


parents: 

diff
changeset




     5


numa = true













87ac093e4d1a
some build cluster resources at TUM;



wenzelm


parents: 

diff
changeset




     6














87ac093e4d1a
some build cluster resources at TUM;



wenzelm


parents: 

diff
changeset




     7


[host.vmnipkow9]








81468






3279f71eb0f4
avoid informatik.tu-muenchen.de domain: soon to be discontinued;



Fabian Huch <huch@in.tum.de>


parents: 
78946

diff
changeset




     8


hostname = "vmnipkow9.in.tum.de"








78946






87ac093e4d1a
some build cluster resources at TUM;



wenzelm


parents: 

diff
changeset




     9














87ac093e4d1a
some build cluster resources at TUM;



wenzelm


parents: 

diff
changeset




    10


[host.mini1]













87ac093e4d1a
some build cluster resources at TUM;



wenzelm


parents: 

diff
changeset




    11


hostname = "131.159.47.71"













87ac093e4d1a
some build cluster resources at TUM;



wenzelm


parents: 

diff
changeset




    12














87ac093e4d1a
some build cluster resources at TUM;



wenzelm


parents: 

diff
changeset




    13


[host.mini2]













87ac093e4d1a
some build cluster resources at TUM;



wenzelm


parents: 

diff
changeset




    14


hostname = "131.159.47.72"













87ac093e4d1a
some build cluster resources at TUM;



wenzelm


parents: 

diff
changeset




    15














87ac093e4d1a
some build cluster resources at TUM;



wenzelm


parents: 

diff
changeset




    16


[host.mini3]













87ac093e4d1a
some build cluster resources at TUM;



wenzelm


parents: 

diff
changeset




    17


hostname = "131.159.46.69"













87ac093e4d1a
some build cluster resources at TUM;



wenzelm


parents: 

diff
changeset




    18














87ac093e4d1a
some build cluster resources at TUM;



wenzelm


parents: 

diff
changeset




    19


[host.studio1]













87ac093e4d1a
some build cluster resources at TUM;



wenzelm


parents: 

diff
changeset




    20


hostname = "131.159.46.182"















isabelle