Editorial: replace non-existent type 'Reference' with type 'Reference Record' and its link

[denlove]

I noticed a bug in ECMAScript specification language types. As far as I know, the word Reference used to be the name of the specification type in the past. According to the specification, the word Record has now been added to these types. I added this word, and the link to the Reference Record also became available.

[linusg]

This is an editorial change, not a normative one.

[denlove]

Yes, editorial, sorry. I wrote one thing and thought of something else.

[denlove]

@linusg, help me, please.

Unfortunately, after renaming the commit, the first job is stuck and cannot be completed. I used dummy commit to reset the progress, but it didn't help me. I can't stop it with no permissions.

[ljharb]

@denlove it's fine, it's just that first-time contributors to repos on github need explicit approval to run workflows.

[denlove]

Like I said, job is stuck and cannot be completed. After 6 hours the first job was cancelled.

[ljharb]

reran.

[denlove]

Thank you for review, Michael.

[safinaskar]

I used dummy commit to reset the progress

Next time just do this: type git commit --amend -a. This command will change timestamp of the last commit. Everything will be the same. Then type git push --force. This is enough to re-run CI. (Note: I'm not contributor to this repo, I'm just a stranger)

[denlove]

Next time just do this: type git commit --amend -a.

@safinaskar . I gotcha 💯, Аскар.

The truth is that your command is almost my recent dummy commit, just bearded men slang. In my version, it was something like that:

git commit --amend --no-edit

Thank you for your advice. I appreciate it. But for me it didn't work even after re-run CI. You can check the logs above.

P.S. ljharb is the best. Thanks. Just paying my respects.

[ljharb]

@denlove oops, forgot a step. would you please register as a contributor?

[denlove]

@ljharb Of course. I've already sent you a request.

[ljharb]

@denlove thanks :-) unfortunately the "github ID" field needs to be a github username, could you fill it out again?

[denlove]

@ljharb Everything is fine?

[ljharb]

awesome, yes, thank you!