Merge Private Master Branch Commits into Public Repo #44
Conversation
…x and run without loading an example)
…pdating the Makefile.
|
Shouldn't the tracer code go away? In particular, why do we need codemirror? |
|
It is already in the public code, that commit was too deep in the branch history for me to bother flattening it out. I agree that tracer can be killed, but it should be in another commit. |
|
Yes, this is the way to go. |
|
Tracer nuked. |
brabalan
left a comment
brabalan
left a comment
There was a problem hiding this comment.
This is looking good. I also asked Marek to take a look.
tilk
left a comment
tilk
left a comment
There was a problem hiding this comment.
Looks good. It doesn't look like any of these changes should break my proofs.
|
Ok, merged into the public branch here, and master of jscert/jscert. I'll now swap 'public' to being the default branch here (and delete master?). Tasks still remaining are to look at merging in #39 and decide which other branches that could possibly be made public candidates are v8, and sublanguages. |
|
Yes, we can abandon (except for issues that need to be closed/transferred), I will lock the master branch from any new accidental pushes. |
As a follow-up to Alan's email to jscert-devel, here's a version of the master branch with the jsjsref work filtered out to minimise the size of the changes to be pushed publicly. (jsjsref history is fully preserved in the jsexplain repository).
There's a few jsjsref directory references in the .gitignore file history and commit history, but I think that's safe to ignore.
We should also look at merging in #39, which is now probably overdue.
Other branches that could possibly be made public are v8, and sublanguages.
I will merge in a tidied version of the condor branch (the improved test harness), once I've removed the junk commits and tested on the Imperial infrastructure.