+ } else if (token == "inzipName") {
+ // this option is currently ignored because only files in
+ // or under current document path is embeddable, and their
+ // inzipName is automatically determined.
+ lex.eatLine();
+ } else if (token == "embed") {
+ lex.next();
+ string const name = lex.getString();
+ filename.setInzipName(name);
+ filename.setEmbed(!name.empty());