Admin/components/nonfree
author wenzelm
Sun, 22 Mar 2020 22:03:48 +0100
changeset 71657 0f98a7c366ed
parent 69386 7bcad752857d
permissions -rw-r--r--
avoid jdk-11.0.6+10: it shows problem "S8217731: Font rendering and glyph spacing changed from jdk-8 to jdk-11" https://bugs.openjdk.java.net/browse/JDK-8217731 even though the changelog claims to have resolved this;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48847
06e8cb8f3f61 some explanations on component categories;
wenzelm
parents: 48843
diff changeset
     1
#special components for internal testing only
48843
9055bf115e30 some grouping of components;
wenzelm
parents:
diff changeset
     2
yices-1.0.28