TextIO.output (outf, ns);
TextIO.output (outf, ".\thostmaster.");
TextIO.output (outf, #domain fs);
- TextIO.output (outf, ".\n( ");
+ TextIO.output (outf, ". ( ");
TextIO.output (outf, Int.toString 123456789);
TextIO.output (outf, " ");
TextIO.output (outf, Int.toString rf);