tools/

This directory contains useful scripts for changing many files at once,
for example replacing string occurences or converting whitespace.