Warning: when download files directly from the website,
the browser might add ".txt" extension automatically to
the files. This makes the code unexecutable or gives wrong results.