@@ -299,8 +299,17 @@ process fn (RmProof n')
299299 let ms = idris_metavars i
300300 putIState $ i { idris_metavars = n : ms }
301301
302−process fn (AddProof prf)
303− = do let fb = fn ++ "~"
302+process fn' (AddProof prf)
303+ = do fn <- do
304+ ex <- liftIO $ doesFileExist fn'
305+ let fnExt = fn' <.> "idr"
306+ exExt <- liftIO $ doesFileExist fnExt
307+ if ex
308+ then return fn'
309+ else if exExt
310+ then return fnExt
311+ else fail $ "Neither \""++fn'++"\" nor \""++fnExt++"\" exist"
312+ let fb = fn ++ "~"
304313 liftIO $ copyFile fn fb -- make a backup in case something goes wrong!
305314 prog <- liftIO $ readFile fb
306315 i <- getIState