tree c36be123da1bca09a17594976f5b19c6e9c9405a
parent 53d41ae8722578c8f3b39e08929c6354211c9c61
author Gilles Peskine <Gilles.Peskine@arm.com> 1564263426 +0200
committer Gilles Peskine <Gilles.Peskine@arm.com> 1568364963 +0200

Remove obsolete options from config.py

These options haven't existed for a long time.