From b97a9ea786fc5f263edc45202382acc3f97d8792 Mon Sep 17 00:00:00 2001 From: Joey Hess Date: Fri, 14 Jun 2013 14:25:17 -0400 Subject: [PATCH] flush stream after each write to update-index, to possibly avoid buffering issues on Windows --- Git/UpdateIndex.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/Git/UpdateIndex.hs b/Git/UpdateIndex.hs index 5d07e20112..76fe0cce91 100644 --- a/Git/UpdateIndex.hs +++ b/Git/UpdateIndex.hs @@ -44,6 +44,7 @@ streamUpdateIndex repo as = pipeWrite params repo $ \h -> do streamer h s = do hPutStr h s hPutStr h "\0" + hFlush h {- A streamer that adds the current tree for a ref. Useful for eg, copying - and modifying branches. -}