On Tue, 2 Apr 2013, David Matthews wrote:
--skip-first-line option: Skip the first line of the input stream. Used with scripts with #! at the start.
You should probably insist in an actual "#!" before skipping the first line, just as a sanity check.
Makarius
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
