Skip to content
Permalink
Browse files

Fix too many open files error

  • Loading branch information...
hirataqdees committed Sep 12, 2019
1 parent f8746ce commit 9632f9daf78d00dd6ae6bacafbdf0947a67e442f
Showing with 3 additions and 0 deletions.
  1. +3 −0 developers/readme_gen.sml
@@ -221,6 +221,7 @@ fun read_block_comment start_comment end_comment filename = let
val all_lines =
map (drop_chars (String.size blank_prefix)) (fst_line :: read_rest ())
val _ = check_length_and_width all_lines
val _ = TextIO.closeIn(f)
in all_lines end handle e => (TextIO.closeIn(f); raise e)
end end;

@@ -256,6 +257,7 @@ fun read_comment_from_script filename = let
val all_lines =
map (drop_chars (String.size prefix)) (fst_line :: read_rest ())
val _ = check_length_and_width all_lines
val _ = TextIO.closeIn(f)
in all_lines end handle e => (TextIO.closeIn(f); raise e)
end;

@@ -276,6 +278,7 @@ fun read_comment_from_raw filename = let
val _ = not (String.isPrefix " " (hd all_lines)) orelse
fail "first line must not start with a blank"
val _ = check_length_and_width all_lines
val _ = TextIO.closeIn(f)
in all_lines end handle e => (TextIO.closeIn(f); raise e)
end;

0 comments on commit 9632f9d

Please sign in to comment.
You can’t perform that action at this time.