-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Made it a bit more sane. Cam up with a concept of a 'task' which is the directory in which the submission script is run. Then renamed variables to reflect this. Also simplified the path variables and did away with it being dependent on your $HOME or whatever. Now the user does that in the noweb.org file and just gives the preceeding path. Also moved out the whole environmental variable section to another noweb insertion point, this makes the script much shorter and comprehendable.
- Loading branch information
Showing
1 changed file
with
151 additions
and
104 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters