Rename demo -> demo.py

This makes sure this script is also detected by the tools used in
tools/check_source.sh.

In general it is not a bad idea to use a file name extension to indicate
the file type. This improves compatibility with other tools in general.

The downside is that command line tools usually should not have a file
name extension. This can be worked around by using symlinks or an
install step. Both can remove the file name extension.

1 files changed, 0 insertions, 0 deletions

diff --git a/demo b/demo.py
index bb9cb98..bb9cb98 100755
--- a/demo
+++ b/demo.py