mirror of
https://github.com/paparazzi/paparazzi.git
synced 2026-05-31 20:38:27 +08:00
[build] only chop extension if it is .xml
This commit is contained in:
committed by
Felix Ruess
parent
3a1624053c
commit
1973131189
@@ -123,7 +123,7 @@ let get_targets_of_module = fun xml ->
|
||||
|
||||
let module_name = fun xml ->
|
||||
let name = ExtXml.attrib xml "name" in
|
||||
try Filename.chop_extension name with _ -> name
|
||||
try if Filename.check_suffix name ".xml" then Filename.chop_extension name else name with _ -> name
|
||||
|
||||
exception Subsystem of string
|
||||
let get_module = fun m global_targets ->
|
||||
|
||||
Reference in New Issue
Block a user