- if (!getOptions().empty())
- file += getOptions() + ' ';
- if (fragile)
- file += "\\protect";
-
- file += "\\url{" + getContents() + '}';
-
+ if (getOptions().empty())
+ os << "[" << getContents() << "]";
+ else
+ os << "[" << getContents() << "||" << getOptions() << "]";