fix rooted_path for win32 (patch from David Powers)
This commit is contained in:
parent
0c09447d00
commit
f56cf4a737
@ -70,10 +70,8 @@ load_foreign_files(Objs,Libs,Entry) :-
|
|||||||
'$checklib_prefix'(NewObjCodes,[0'l,0'i,0'b|NewObjCodes]).
|
'$checklib_prefix'(NewObjCodes,[0'l,0'i,0'b|NewObjCodes]).
|
||||||
|
|
||||||
'$rooted_path'([C|_]) :- '$dir_separator'(C), !.
|
'$rooted_path'([C|_]) :- '$dir_separator'(C), !.
|
||||||
'$rooted_path'(Cs) :-
|
% windows drive z:\
|
||||||
% win32 machine
|
'$rooted_path'([_,0':,0'\\|_]) .
|
||||||
'$dir_separator'(0'\\),
|
|
||||||
'$get_drive'(Cs).
|
|
||||||
|
|
||||||
'$get_drive'([0':|_]) :- !.
|
'$get_drive'([0':|_]) :- !.
|
||||||
'$get_drive'([0'\\|_]) :- !, fail.
|
'$get_drive'([0'\\|_]) :- !, fail.
|
||||||
|
Reference in New Issue
Block a user