Mirrors_Framework/paparazzi
1
0
Fork 0
mirror of https://github.com/paparazzi/paparazzi.git synced 2026-06-07 00:53:41 +08:00
Code Issues Actions 25 Packages Projects Releases Wiki Activity

fix bug occuring with unexpected filenames in var/maps

Browse Source
This commit is contained in:
Pascal Brisset
2009-09-24 17:13:58 +00:00
parent f0b11f7e2d
commit af039f5238
1 changed files with 3 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files
sw/lib/ocaml/gm.ml
+3 -3
View File
@@ -145,10 +145,10 @@ let get_from_cache = fun f ->
let rec loop = fun i ->
if i < Array.length files then
let fi = files.(i) in
let fi_key = Filename.chop_extension fi in
if try is_prefix fi_key f with _ -> false then begin
let fi_key = try Filename.chop_extension fi with _ -> fi in
if fi_key <> "" && is_prefix fi_key f then
(tile_of_key fi_key, !cache_path // fi)
end else
else
loop (i+1)
else
raise Not_found in