#!/bin/sh

# Temporary README extractor

cat doc/html/files.html				\
| sed 's/<[^>]*>//g; s/^ *//g'		\
| grep ^platon						\
| sed 's/\[code\]/-- /g';