Fixing a bug in ExtractorScript.py: consuming too many tokens.