@@ -900,14 +900,15 @@ process h fn (RmProof n')
901process h fn' (AddProof prf)
901process h fn' (AddProof prf)
902 = do fn <- do
902 = do fn <- do
903+ let fn'' = takeWhile (/= ' ') fn'
903− ex <- runIO $ doesFileExist fn'
904+ ex <- runIO $ doesFileExist fn''
904− let fnExt = fn' <.> "idr"
905+ let fnExt = fn'' <.> "idr"
905 exExt <- runIO $ doesFileExist fnExt
906 exExt <- runIO $ doesFileExist fnExt
907− then return fn'
908+ then return fn''
908 else if exExt
909 else if exExt
909 then return fnExt
910 then return fnExt
910− else ifail $ "Neither \""++fn'++"\" nor \""++fnExt++"\" exist"
911+ else ifail $ "Neither \""++fn''++"\" nor \""++fnExt++"\" exist"
911 let fb = fn ++ "~"
912 let fb = fn ++ "~"
912 runIO $ copyFile fn fb -- make a backup in case something goes wrong!
913 runIO $ copyFile fn fb -- make a backup in case something goes wrong!
913 prog <- runIO $ readFile fb
914 prog <- runIO $ readFile fb