Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
clean-and-itasks
clean-ide
Commits
f0fbdce0
Commit
f0fbdce0
authored
Feb 13, 2002
by
Diederik van Arkel
Browse files
remove unused uniqueness
parent
fe4d6777
Changes
2
Hide whitespace changes
Inline
Side-by-side
Win/Platform.dcl
View file @
f0fbdce0
...
@@ -13,5 +13,5 @@ TooltempDir :: String
...
@@ -13,5 +13,5 @@ TooltempDir :: String
EnvsDir
::
String
EnvsDir
::
String
PrefsDir
::
String
PrefsDir
::
String
batchOptions
::
!*
World
->
(!
Bool
,
!
Bool
,
!
String
,
!
*
File
,!*
World
)
batchOptions
::
!*
World
->
(!
Bool
,
Bool
,
String
,*
File
,!*
World
)
wAbort
::
!
String
!*
World
->
*
World
wAbort
::
!
String
!*
World
->
*
World
Win/Platform.icl
View file @
f0fbdce0
...
@@ -54,7 +54,7 @@ initPlatformCommandLine ps
...
@@ -54,7 +54,7 @@ initPlatformCommandLine ps
#
files
=
map
GetLongPathName
files
#
files
=
map
GetLongPathName
files
=
(
files
,
ps
)
=
(
files
,
ps
)
batchOptions
::
!*
World
->
(!
Bool
,
!
Bool
,
!
String
,
!
*
File
,!*
World
)
batchOptions
::
!*
World
->
(!
Bool
,
Bool
,
String
,*
File
,!*
World
)
batchOptions
world
batchOptions
world
=
case
[
arg
\\
arg
<-:
getCommandLine
]
of
=
case
[
arg
\\
arg
<-:
getCommandLine
]
of
[_,
"--batch-build"
,
prj
]
[_,
"--batch-build"
,
prj
]
...
@@ -73,7 +73,7 @@ where
...
@@ -73,7 +73,7 @@ where
wAbort
::
!
String
!*
World
->
*
World
wAbort
::
!
String
!*
World
->
*
World
wAbort
message
world
wAbort
message
world
#
stderr
=
fwrites
message
stderr
#
stderr
=
fwrites
message
stderr
//
# (_,world) = fclose stderr world
#
(_,
world
)
=
fclose
stderr
world
#
world
=
set_return_code_world
(
-1
)
world
#
world
=
set_return_code_world
(
-1
)
world
=
world
=
world
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment