jdk/src/share/classes/java/util/logging/StreamHandler.java
changeset 14216 23714b376286
parent 5506 202f599c92aa
child 14333 65fe875afb41
equal deleted inserted replaced
13644:063cbb0da3d3 14216:23714b376286
   247             }
   247             }
   248         }
   248         }
   249     }
   249     }
   250 
   250 
   251     private synchronized void flushAndClose() throws SecurityException {
   251     private synchronized void flushAndClose() throws SecurityException {
   252         checkAccess();
   252         checkPermission();
   253         if (writer != null) {
   253         if (writer != null) {
   254             try {
   254             try {
   255                 if (!doneHeader) {
   255                 if (!doneHeader) {
   256                     writer.write(getFormatter().getHead(this));
   256                     writer.write(getFormatter().getHead(this));
   257                     doneHeader = true;
   257                     doneHeader = true;