Peter Schneider-Kamp:

Peter Schneider-Kamp:

Problem:
A Python program can be completed and reformatted using
Tools/scripts/pindent.py. Unfortunately there is no option for removal
of the generated "# end"-tags.  Although a few Python commands or a
"grep -v '# end '" can do wonders here, there are two drawbacks:
- not everyone has grep/time to write a Python script
- it is not checked whether the "# end"-tags were used validly

Solution:
add extra option "-e" (eliminate) to pindent.py