tree 2823c27e2728eac14245d7ff03b2b737a7d44368
parent e3734bd13ab98ef4c18729522b43d8d0a82774ea
author Gilles Peskine <Gilles.Peskine@arm.com> 1567630307 +0200
committer Gilles Peskine <Gilles.Peskine@arm.com> 1568365464 +0200

Fix config.py output when a symbol has acquired or lost a value

Normally a valueless symbol remains valueless and a symbol with a
value keeps having one. But just in case a symbol does get changed
from valueless to having a value, make sure there's a space between
the symbol and the value. And if a symbol gets changed from having a
value to valueless, strip trailing whitespace.

Add corresponding tests.

Also fix the case of a valueless symbol added with the set method,
which would have resulted in attempting to use None as a string. This
only happened with the Python API, not with the command line API.